PartitionHelpers.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

28 declarations, 0 contain sorry, 0 declared as axioms

Sylow `p`-subgroup lemmas for finite subgroups of `PGL₂(𝔽̄_p)`

This file proves the basic facts about Sylow p-subgroups of a finite subgroup G of PGLOf (K p) = PGL₂(𝔽̄_p) whose order is divisible by p (the wild case of Dickson's classification).

The key geometric input is that an element of order p in PGLOf (K p) fixes exactly one point of the projective line. From this we deduce:

each Sylow p-subgroup P of G fixes a unique point sylowFixedPoint of ℙ¹(𝔽̄_p), and distinct Sylow p-subgroups have distinct fixed points (Dickson.sylow_fixedPoint_injective);
distinct Sylow p-subgroups intersect trivially (Dickson.sylow_pairwise_trivial_intersection);
a count of the elements of order dividing p in G (Dickson.count_order_p_elements);
the normalizer of P in G is the stabilizer of its fixed point, and numerical consequences for |G| (Dickson.normalizer_complement_divides_main, Dickson.group_order_gt_normalizer).

Imports (2)

Imported by 3 files

theorem Dickson.sylow_card_prime_pow line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Exists, And and 3 more
Proof uses: Exists.intro, Finsupp, Nat.factorization, And.intro, Nat.pos_of_ne_zero, Iff.mp, Finset, Finsupp.support, Ne, Finsupp.mem_support_iff, Iff.mpr, Nat.primeFactors, Nat.mem_primeFactors, Fact.out, LT.lt.ne', Nat.card_pos, Sylow.card_eq_multiplicity
55 instances, coercions and auxiliary constants left out.
theorem Dickson.sylow_card_ge_3 line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, GE.ge
Proof uses: And, Eq, HPow.hPow, Exists, Dickson.sylow_card_prime_pow, Eq.mpr, id, congrArg, LE.le.trans, Nat.succ, Nat.succ_le_of_lt, Fact.out, Nat.le_self_pow
48 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_unique_fixedPoint line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, ExistsUnique and 5 more
Proof uses: Equiv, MulEquiv.toEquiv, Subgroup.equivMapOfInjective, Subtype.coe_injective, Finite.of_equiv, And.right, Monoid.exponent, HMul.hMul, And, Dickson.isPGroup_comm_exponent_fixedPoint, IsPGroup.map, Sylow.isPGroup', Decidable.byContradiction, Nontrivial, Not, Unique, Unique.mk, Inhabited.mk, by_contra, Inhabited.default and 76 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Dickson.normalizer_stabilizes_fixedPoint line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Sylow, Dickson.ProjectiveLine, Eq, HSMul.hSMul, Subgroup.normalizer
Proof uses: Inv.inv, Eq.mpr, HMul.hMul, id, congrArg, Eq.symm, SemigroupAction.mul_smul, of_eq_true, Eq.trans, True, congrFun', inv_mul_cancel, one_mul, eq_self, Iff.mp, Set, Eq.refl, congr_arg, smul_inv_smul
63 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_element_order_p line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Sylow, Ne, Eq, orderOf
Proof uses: Subgroup.map, Subgroup.subtype, Finite.of_equiv, MulEquiv.toEquiv, Subgroup.equivMapOfInjective, Subtype.coe_injective, Dickson.isPGroup_orderOf_eq_prime, IsPGroup.map, Sylow.isPGroup', Subtype.mk, Subgroup.mem_map_of_mem, Subtype.ext, congr_arg
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Dickson.order_p_one_fixedPoint line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Eq, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Set.ncard, Dickson.ProjectiveLine, Dickson.fixedPoints
Proof uses: Iff.mpr, And.left, Iff, Nat.Coprime, Dickson.fixedPoints_dichotomy, Nat.Prime.ne_one, Fact.out, Eq.trans, Eq.symm, congr_arg, orderOf_one, Iff.mp, LT.lt, IsOfFinOrder, orderOf_pos_iff, Eq.rec, Nat.Prime.pos
37 instances, coercions and auxiliary constants left out.
def Dickson.sylowFixedPoint The unique fixed point on the projective line ℙ¹(𝔽̄_p) of a Sylow p-subgroup P line 116 source
Source documentation
The unique fixed point on the projective line ℙ¹(𝔽̄_p) of a Sylow p-subgroup P.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Dickson.ProjectiveLine
Proof uses: Exists.choose, And, Subgroup.map, Subgroup.subtype, Eq, HSMul.hSMul, Dickson.sylow_unique_fixedPoint
39 instances, coercions and auxiliary constants left out.
```
noncomputable def sylowFixedPoint (G : Subgroup (PGLOf (K p))) [Finite G]
    (hG_p : p ∣ Nat.card G) (P : Sylow p G) : ProjectiveLine p :=
…
```
Mentions: Dickson.PGLOf, Dickson.K, Dickson.ProjectiveLine
theorem Dickson.sylow_element_fixes line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Eq and 3 more
Proof uses: And.left, Subgroup.map, Subgroup.subtype, Exists.choose, And, Dickson.sylow_unique_fixedPoint, Exists.choose_spec, Subgroup.mem_map_of_mem
44 instances, coercions and auxiliary constants left out.
theorem Dickson.eq_sylow_fixedPoint line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Dickson.ProjectiveLine and 3 more
Proof uses: And.right, Subgroup.map, Subgroup.subtype, Exists.choose, And, Dickson.sylow_unique_fixedPoint, Exists.choose_spec, MonoidHom, Exists, Iff.mp, Subgroup.mem_map
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.shared_element_shared_fixedPoint line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Ne and 3 more
Proof uses: Set, Dickson.fixedPoints, Singleton.singleton, Exists, Iff.mp, Set.ncard, Set.ncard_eq_one, Dickson.order_p_one_fixedPoint, Dickson.sylow_element_order_p, Eq.trans, Iff, Set.ext_iff, Dickson.sylow_element_fixes, Eq.symm
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_pairwise_trivial_intersection line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Ne and 3 more
Proof uses: Decidable.byContradiction, Not, And, Exists, False, Subgroup.ext, Iff.intro, by_contra, Exists.intro, And.intro, Eq.rec, Set, Submonoid, Subgroup.toSubmonoid, Subgroup.one_mem, Eq.symm, Iff.mp, Subgroup.mem_bot, HMul.hMul, dite and 42 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
theorem Dickson.count_order_p_elements line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Eq and 6 more
Proof uses: Set, Set.iUnion, Finset, Finset.univ, SDiff.sdiff, Singleton.singleton, Set.ext, Eq.mpr, Iff, Exists, And, Not, id, congrArg, Eq.trans, True, congrFun', funext, Set.iUnion_congr_Prop, Iff.of_eq and 88 more
152 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
theorem Dickson.fixes_infinity_commutes_order_p line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, HMul.hMul, Or
Proof uses: Exists, Ne, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Iff.mp, Dickson.fixesInfinity_iff_upperTriangular, Dickson.isUnipotent_of_fixesInfinity_orderOf, Nat.Prime.ne_one, Fact.out, Eq.trans, Eq.symm, congr_arg, Eq.mpr, id, congrArg, Membership.mem, Subgroup and 107 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 89 steps
Open to load the checked before-and-after goal states.
theorem Dickson.common_fixedPoint_commutes_order_p line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Dickson.ProjectiveLine, Eq, HSMul.hSMul, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, HMul.hMul, Or
Proof uses: Dickson.infinity, Exists, Dickson.exists_smul_eq_infinity, Inv.inv, Eq.mpr, id, congrArg, Eq.symm, SemigroupAction.mul_smul, inv_smul_smul, Eq.refl, MulEquiv, MonoidHom, MulAut, MulAut.conj, map_mul, orderOf_injective, MulEquiv.toMonoidHom, MulEquiv.injective, Dickson.fixes_infinity_commutes_order_p and 1 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Dickson.order_one_or_p_in_sylow line 373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Subgroup.normalizer, Or and 2 more
Proof uses: IsPGroup, Subgroup.zpowers, Eq.mpr, Exists, HPow.hPow, id, congrArg, propext, IsPGroup.iff_card, Nat.card_zpowers, Eq.symm, Subgroup.orderOf_coe, Or.elim, Exists.intro, pow_zero, Eq.refl, pow_one, Eq.rec, Max.max, Subgroup.mem_sup_left and 8 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Dickson.normalizer_fixes_element_in_sylow line 386 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Subgroup.normalizer and 4 more
Proof uses: Eq.mpr, id, congrArg, Eq.symm, mul_one, inv_mul_cancel, mul_assoc, Eq.refl, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.sylowFixedPoint, Dickson.normalizer_stabilizes_fixedPoint, Dickson.sylow_element_fixes, Dickson.eq_sylow_fixedPoint, Or, orderOf, Dickson.common_fixedPoint_commutes_order_p, Dickson.sylow_element_order_p, congr_arg, Dickson.order_one_or_p_in_sylow
67 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance Dickson.conjOnP line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Sylow, Subtype, Membership.mem, MulAction, Subgroup.normalizer
Proof uses: MulAction.mk, SemigroupAction.mk, SMul.mk, Subtype.mk, HMul.hMul, Inv.inv
54 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Dickson.stabilizer_conj_eq_P line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Ne and 4 more
Proof uses: Subgroup.map, Subgroup.subtype, Set.Finite.to_subtype, Set.Finite.subset, Set.range, MonoidHom, Set.finite_range, Set, And, Set.mem_range_self, HMul.hMul, Inv.inv, And.left, Monoid.exponent, ExistsUnique, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.isPGroup_comm_exponent_fixedPoint, IsPGroup.map, Sylow.isPGroup' and 17 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Dickson.normalizer_complement_divides_main line 441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Sylow, Dvd.dvd, Nat.card, HDiv.hDiv and 2 more
Proof uses: Fintype, Fintype.ofFinite, MulAction, SMul, Ne, Eq, MulAction.orbit, Nonempty, MulAction.stabilizer, Nonempty.intro, Equiv, Subgroup.subgroupOf, Equiv.mk, Subtype.mk, Subtype.property, Subgroup.le_normalizer, rfl, Eq.mpr, id, congrArg and 70 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
def Dickson.normalizerQuotient The index |N_G(P)| / |P| of a Sylow p-subgroup P in its normalizer in G line 493 source
Source documentation
The index |N_G(P)| / |P| of a Sylow p-subgroup P in its normalizer in G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Sylow
Proof uses: HDiv.hDiv, Nat.card, Subgroup.normalizer
36 instances, coercions and auxiliary constants left out.
```
def normalizerQuotient (G : Subgroup (PGLOf (K p))) [Finite G]
    (P : Sylow p G) : ℕ :=
…
```
Mentions: Dickson.PGLOf, Dickson.K
theorem Dickson.group_order_gt_normalizer line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Sylow, GT.gt, Fintype.card, Dickson.instFintypeSylow, Nat.card and 2 more
Proof uses: Eq, HasQuotient.Quotient, Subgroup.normalizer, Eq.trans, Eq.symm, Nat.card_congr, Sylow.equivQuotientNormalizer, Nat.card_eq_fintype_card, Eq.mpr, HDiv.hDiv, id, congrArg, Dickson.normalizerQuotient.eq_1, Nat.mul_div_cancel', Subgroup.card_dvd_of_le, Subgroup.le_normalizer, Subgroup.card_eq_card_quotient_mul_card_subgroup, LT.lt, Nat.mul_lt_mul_of_pos_right, Nat.card_pos and 2 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Dickson.not_dvd_pred_pow line 524 source
standard axioms: propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Not, Dvd.dvd, HSub.hSub, HPow.hPow
Proof uses: HAdd.hAdd, Eq.mpr, id, Eq, congrArg, Nat.sub_add_cancel, Nat.one_le_pow, Nat.Prime.pos, Fact.out, dvd_pow_self, ne_of_gt, Nat.Prime.not_dvd_one, Iff.mp, Nat.dvd_add_right
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Dickson.factorization_pgl_order line 534 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Eq, Finsupp, Nat.factorization, HMul.hMul, HPow.hPow, HSub.hSub
Proof uses: Eq.mpr, Or, Not, Dvd.dvd, id, congrArg, propext, Nat.factorization_eq_zero_iff, Or.inr, Or.inl, Dickson.not_dvd_pred_pow, Nat.mul_pos, Nat.succ_pos, HAdd.hAdd, Nat.factorization_mul_of_coprime, Nat.Coprime.pow_left, Nat.Coprime, Nat.Prime.coprime_iff_not_dvd, Fact.out, Finsupp.single and 4 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_order_of_pgl_order line 548 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, Eq, Nat.card, HMul.hMul, HPow.hPow and 2 more
Proof uses: Eq.mpr, Finsupp, Nat.factorization, id, congrArg, Sylow.card_eq_multiplicity, Dickson.factorization_pgl_order, Eq.refl
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_fixedPoint_injective line 555 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Function.Injective, Sylow and 2 more
Proof uses: Eq, Decidable.byContradiction, Not, HMul.hMul, Subtype.ext, dite, Eq.mpr, id, congrArg, Commute.one_left, Commute.one_right, Dickson.commute_of_orderOf_prime_common_fixedPoint, Dickson.sylow_element_order_p, Dickson.sylow_element_fixes, Eq.rec, HSMul.hSMul, Eq.symm, Max.max, Exists, And and 63 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_free_action line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, Ne and 3 more
Proof uses: Eq, Set, Dickson.fixedPoints, Singleton.singleton, Exists, False, Iff.mp, Set.ncard, Set.ncard_eq_one, Dickson.order_p_one_fixedPoint, Dickson.sylow_element_order_p, Dickson.sylow_element_fixes, Dickson.sylow_fixedPoint_injective, Eq.trans, Eq.mp, congrArg, propext, Set.mem_singleton_iff, Eq.symm
51 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Dickson.card_sylow_mod_card line 623 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Sylow, HSub.hSub and 2 more
Proof uses: Finset, SDiff.sdiff, Eq, Finset.univ, Singleton.singleton, rfl, Ne, HSMul.hSMul, Dickson.order_one_or_p_in_sylow, Iff.mp, Subgroup.normalizer, Sylow.smul_eq_iff_mem_normalizer, Or.inr, orderOf, Dickson.sylow_element_order_p, Dickson.sylow_fixedPoint_injective, Dickson.shared_element_shared_fixedPoint, And.right, Not, And and 64 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
theorem Dickson.n_p_eq_pgl line 670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, GE.ge, Eq, Nat.card, HMul.hMul and 6 more
Proof uses: Nonempty, inferInstance, Dvd.dvd, Eq.rec, Dickson.card_sylow_mod_card, dvd_mul_of_dvd_left, dvd_pow_self, ne_of_gt, Eq.symm, Dickson.sylow_order_of_pgl_order, Exists, Exists.intro, HDiv.hDiv, Eq.mpr, id, congrArg, Nat.div_mul_cancel, Nat.sub_add_cancel, LT.lt.le, Eq.refl and 56 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.

FLT/Slop/PGL2/FiniteSubgroups/PartitionHelpers.lean

Sylow p-subgroup lemmas for finite subgroups of PGL₂(𝔽̄_p)

`FLT/Slop/PGL2/FiniteSubgroups/PartitionHelpers.lean`

Sylow `p`-subgroup lemmas for finite subgroups of `PGL₂(𝔽̄_p)`