Homotopy Finiteness

This webpage is a mirror of the formalisation of Rijke's proof that the number of groups of finite order is finite in Jonas Hoefer's prototype, offered to have a better viewing experience than on the GitHub.

You can start consulting the files by one of the following:

• GroupFiniteness.html: the application of homotopy finiteness to groups.
• HomotopyFiniteness.html: the main proof of this formalization.

Then, in each file, the imports are linked to facilitate browsing.