Fermat's Last Theorem in Lean 4

Namespace `MulAction` 4 theorems

Orbit intersection count for a factorised transitive group action MulAction.ncard_orbit_inter_orbit_mul_card 0 below · cited by 1 · depth 11
Orbit count for an action of a group of prime order MulAction.card_mul_natCard_orbitRel_quotient_eq_of_natCard_eq_prime 0 below · cited by 5 · depth 12
Marks of a tetrahedral group on a transitive set MulAction.natCard_fixedBy_of_isPretransitive_of_card_eq_twelve 0 below · cited by 2 · depth 15
Cyclic C-sets are determined by elementwise fixed-point counts MulAction.exists_equiv_map_smul_of_card_fixedBy_eq_of_isCyclic 0 below · cited by 1 · depth 18

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.