Second Sylow Theorem in Naproche / ForTheL

This repository contains files that can be interpreted as a proof of Sylow's Second Theorem by Naproche-SAD.
The proof is based on a lecture held by Prof. Dr. Jan Schröer at the University of Bonn in 2019/20.

There exists a formalization in LEAN.

The Proof

The formalized proof is divided into eight files located in /PROOF/:

• 01basicgrptheory.ftl
    Introduction of groups, subgroups and cosets
• 02numbers.ftl
    Axiomatic introduction of natural numbers and integers
• 03cards.ftl
    Axiomatic introduction of finite sets and finite cardinalities
• 04lagrange.ftl
    Proof of Lagrange's Theorem
• 05staborb.ftl
    Bijection between stabilizers and orbits
• 06fixedpointsmodp.ftl
    Properties of fixed points of group actions
• 07grpaction.ftl
    Definition of the group action used in the following proof
• 08sylow2.ftl
    Proof of Sylow's Second Theorem

The files have been verified in Isabelle - Naproche on a MacBook Pro with an 2,7 GHz Quad-Core Intel Core i7 and 16 GB of RAM in approximately 5 minutes.

Formalization in Lean

A formalization in LEAN based on ChrisHughes24/Sylow can be found at moritz-hl/sylowlean.