PartitionProof.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

30 declarations, 0 contain sorry, 0 declared as axioms

The partition equation for wild finite subgroups of `PGL₂(𝔽̄_p)`

Let G be a finite subgroup of PGLOf (K p) = PGL₂(𝔽̄_p) with p dividing |G|. This file studies the set Dickson.Phi G ⊆ ℙ¹(𝔽̄_p) of fixed points of nontrivial elements of G, via a double-counting (Burnside/orbit-counting) argument on the action of G on Phi G.

The main results are:

Dickson.num_orbits_eq_two: if G is not cyclic of order p then... in fact under the standing hypotheses the action of G on Phi G has exactly two orbits;
Dickson.card_eq_pm_z1_np': the resulting numerical relation |G| = n_p * (z₁ * (n_p - 1) + n_p)-style partition identity expressing |G| in terms of the number n_p of Sylow p-subgroups and the order z₁ of the cyclic complement, which drives the case analysis in the wild classification.

Imports (4)

Imported by 2 files

def Dickson.Phi The set of points on the projective line fixed by some non-identity element of G line 56 source
Source documentation
The set of points on the projective line fixed by some non-identity element of 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, Set, Dickson.ProjectiveLine
Proof uses: Set.iUnion, Subtype, Membership.mem, Ne, Set.ofPred, Eq, HSMul.hSMul
33 instances, coercions and auxiliary constants left out.
```
def Phi (G : Subgroup (PGLOf (K p))) : Set (ProjectiveLine p) :=
…
```
Mentions: Dickson.PGLOf, Dickson.K, Dickson.ProjectiveLine
lemma Dickson.Phi_finite line 60 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, Set.Finite, Dickson.ProjectiveLine, Dickson.Phi
Proof uses: Set.Finite.biUnion, Eq, False, Set.toFinite, Set, Set.ofPred, HSMul.hSMul, IsOfFinOrder, And, LT.lt, HPow.hPow, Exists, Iff.mp, isOfFinOrder_iff_pow_eq_one, isOfFinOrder_of_finite, Iff.mpr, Exists.intro, And.intro, Subtype.ext_iff, Iff and 20 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Dickson.Phi_smul_mem line 76 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, Subtype, Membership.mem, Dickson.ProjectiveLine, Set, Dickson.Phi, HSMul.hSMul
Proof uses: Eq.mpr, Exists, Ne, Eq, id, Eq.trans, Set.iUnion, Set.ofPred, congrArg, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl, Eq.mp, Exists.intro, HMul.hMul, Inv.inv, Eq.symm, inv_mul_cancel_left and 7 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev Dickson.PhiType The subtype of points on the projective line fixed by some non-identity element of G line 88 source
Source documentation
The subtype of points on the projective line fixed by some non-identity element of 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
Proof uses: Dickson.ProjectiveLine, Dickson.Phi
27 instances, coercions and auxiliary constants left out.
```
abbrev PhiType (G : Subgroup (PGLOf (K p))) := ↥(Phi p G)
```
Mentions: Dickson.PGLOf, Dickson.K, Dickson.Phi
instance Dickson.phiFintype line 90 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, Fintype, Dickson.PhiType
Proof uses: Set.Finite.fintype, Dickson.ProjectiveLine, Dickson.Phi, Dickson.Phi_finite
32 instances, coercions and auxiliary constants left out.
instance Dickson.phiMulAction line 94 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, MulAction, Subtype, Membership.mem, Dickson.PhiType
Proof uses: MulAction.mk, SemigroupAction.mk, SMul.mk, Subtype.mk, Dickson.ProjectiveLine, Set, Dickson.Phi, HSMul.hSMul
47 instances, coercions and auxiliary constants left out.
lemma Dickson.sylow_fixedPt_mem_Phi line 100 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, Ne, Exists, Decidable.byContradiction, Eq, HMul.hMul, Not, absurd, GE.ge, False, Dickson.sylow_card_ge_3, Eq.mpr, Bot.bot, id, congrArg, Iff.mpr, LE.le, eq_bot_iff, Eq.mp, Eq.trans and 26 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Dickson.Phi_card_le line 111 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, LE.le, Fintype.card, Dickson.PhiType, HMul.hMul and 2 more
Proof uses: Ne, Set.ncard, Dickson.ProjectiveLine, Set.ofPred, Eq, HSMul.hSMul, And, Iff, Dickson.fixedPoints, orderOf, Nat.Coprime, Dickson.fixedPoints_dichotomy, Subtype.ext, Iff.mpr, IsOfFinOrder, Submonoid, Subgroup.toSubmonoid, Submonoid.isOfFinOrder_coe, isOfFinOrder_of_finite, Or and 63 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_distinct_fixedPoints 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 2 more
Proof uses: Eq, HMul.hMul, dite, Eq.mpr, id, congrArg, one_mul, mul_one, Eq.refl, Not, Subtype.ext, Dickson.commute_of_orderOf_prime_common_fixedPoint, Submonoid, Subgroup.toSubmonoid, Dickson.sylow_element_order_p, Eq.rec, HSMul.hSMul, Dickson.sylow_element_fixes, Subgroup.mk, Submonoid.mk and 45 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
theorem Dickson.fixes_sylowPoint_normalizes line 197 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 4 more
Proof uses: Eq.mpr, Iff, HMul.hMul, Inv.inv, id, congrArg, propext, Subgroup.mem_normalizer_iff, Subgroup.map, MulAut, MonoidHom, MulAut.conj, Decidable.byContradiction, Not, Dickson.sylow_distinct_fixedPoints, Eq.symm, Dickson.eq_sylow_fixedPoint, And, Exists, Iff.mp and 31 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem Dickson.stabilizer_sylowFixedPoint_eq_normalizer line 226 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: Dickson.normalizer_stabilizes_fixedPoint, Dickson.sylow_element_fixes, Dickson.eq_sylow_fixedPoint, Set.ext, Iff.intro, Dickson.fixes_sylowPoint_normalizes
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_fixedPt_injective line 236 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 6 more
Proof uses: Eq, Iff.mp, Not, not_imp_not, Dickson.sylow_distinct_fixedPoints, Subtype.ext_iff
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Dickson.fixedBy_eq_fixedPoints line 245 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, Ne, Eq, Fintype.card, Dickson.PhiType and 6 more
Proof uses: Eq.mpr, Nat.card, id, congrArg, Eq.symm, Nat.card_eq_fintype_card, Nat.card_coe_set_eq, Nat.card_congr, Equiv.mk, Subtype.mk, Iff.mp, HSMul.hSMul, Subtype.ext_iff, Subtype.property, Iff.mpr, Set.iUnion, Set.ofPred, Exists, Set.mem_iUnion, Exists.intro and 2 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.count_elements_order_p line 257 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 8 more
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Dickson.count_order_p_elements, Eq.rec, Eq.refl, Set, funext, propext, Iff, Subgroup.orderOf_coe, and_iff_right_of_imp, False, Nat.Prime.ne_one, Fact.out, Eq.mp, orderOf_one
65 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Dickson.element_fixedPt_sum line 269 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, Fintype and 12 more
Proof uses: eq_tsub_of_add_eq, HAdd.hAdd, Finset, ite, orderOf, Ne, Finset.ne_of_mem_erase, And, Iff, Nat.Coprime, Dickson.fixedPoints_dichotomy, Subtype.ext, Iff.mpr, IsOfFinOrder, Submonoid, Subgroup.toSubmonoid, Submonoid.isOfFinOrder_coe, isOfFinOrder_of_finite, dite, Eq.mpr and 35 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Dickson.phi_stab_card_ge_two line 311 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, Dickson.PhiType, LE.le, Nat.card, MulAction.stabilizer
Proof uses: Exists, Ne, Dickson.ProjectiveLine, Set, Set.ofPred, Eq, HSMul.hSMul, Dickson.Phi, Iff.mp, Set.iUnion, Set.mem_iUnion₂, Subtype.prop, Trans.trans, Insert.insert, Singleton.singleton, Set.ncard, Eq.symm, Set.ncard_pair, Nat.card_coe_set_eq, Nat.card_mono and 13 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Dickson.orbit_count_mul_card line 324 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, Eq, HMul.hMul, Fintype.card, Quotient and 7 more
Proof uses: Eq.mpr, Dickson.ProjectiveLine, Set, Dickson.Phi, id, congr, congrArg, Nat.card_eq_fintype_card, Finset.sum_congr, Eq.refl, Finset, MulAction.fixedBy, Eq.symm, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, Finset.card, Finset.filter, Fintype.card_subtype, Finset.bipartiteAbove, HSMul.hSMul, Finset.bipartiteBelow and 1 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Dickson.nonsplit_D_lt_n line 333 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, Fintype.card and 5 more
Proof uses: GE.ge, Dickson.sylow_card_ge_3, LE.le, Nat.le_of_dvd, Nat.sub_pos_of_lt, Dickson.card_sylow_mod_card, Decidable.byContradiction, Not, And, And.intro, Subgroup.card_subgroup_dvd_card, Eq.mpr, id, Eq, congrArg, Eq.symm, Nat.card_eq_fintype_card, HasQuotient.Quotient, Subgroup.normalizer, Nat.card_congr and 86 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Dickson.fixedBy_sum_eq line 357 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, Fintype and 14 more
Proof uses: Fintype.card_congr, Equiv.subtypeUnivEquiv, one_smul, Eq.mpr, Insert.insert, Finset, Finset.erase, id, congrArg, Eq.symm, Finset.insert_erase, Finset.mem_univ, Finset.sum_insert, Finset.notMem_erase, Set.ncard, Dickson.fixedPoints, Finset.sum_congr, rfl, Dickson.fixedBy_eq_fixedPoints, Finset.ne_of_mem_erase and 2 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Dickson.stab_sum_eq_phi_plus_element line 373 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 9 more
Proof uses: Eq.mpr, Dickson.ProjectiveLine, Set, Dickson.Phi, id, congrArg, Finset.sum_congr, rfl, Finset, Nat.card_eq_fintype_card, MulAction.fixedBy, Finset.card, Finset.filter, congr, Eq.refl, Fintype.card_subtype, Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, HSMul.hSMul, Fintype.ofFinite, Dickson.fixedBy_sum_eq
75 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_orbit_size line 387 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 9 more
Proof uses: Dickson.PhiType, MulAction.stabilizer, Subgroup.normalizer, SetLike.ext, Iff.trans, HSMul.hSMul, Subtype.ext_iff, Iff.mp, Set.ofPred, Iff, Set.ext_iff, Dickson.stabilizer_sylowFixedPoint_eq_normalizer, Eq.mpr, id, congrArg, Eq.symm, Nat.card_eq_fintype_card, HasQuotient.Quotient, Nat.card_congr, MulAction.orbitEquivQuotientStabilizer and 1 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_fixedPt_phiStab line 400 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.PhiType and 11 more
Proof uses: Eq.symm, Nat.div_eq_of_eq_mul_left, Iff.mpr, LT.lt, Nonempty, Fintype.card_pos_iff, Nonempty.intro, Eq.mpr, HMul.hMul, id, congrArg, mul_comm, MulAction.orbit, Dickson.sylow_orbit_size, congr, Nat.card_eq_fintype_card, MulAction.card_orbit_mul_card_stabilizer_eq_card_group
67 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Dickson.stab_sum_lower_bound line 411 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 and 9 more
Proof uses: Subtype.mk, Dickson.ProjectiveLine, Set, Dickson.Phi, Dickson.sylowFixedPoint, Dickson.sylow_fixedPt_mem_Phi, Finset, Finset.image, Eq, Function.Injective, Dickson.sylow_fixedPt_injective, SDiff.sdiff, Eq.trans, Eq.symm, Finset.sum_sdiff, Finset.subset_univ, add_comm, Eq.mpr, id, congrArg and 24 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Dickson.num_orbits_eq_two line 447 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, Fintype.card and 6 more
Proof uses: HMul.hMul, HAdd.hAdd, HSub.hSub, Eq.mpr, Finset.sum, Finset.univ, MulAction.stabilizer, id, congrArg, Dickson.orbit_count_mul_card, Dickson.stab_sum_eq_phi_plus_element, Eq.refl, LE.le, Dickson.stab_sum_lower_bound, Dickson.Phi_card_le, Fintype.card_le_of_injective, Subtype.mk, Dickson.ProjectiveLine, Set, Dickson.Phi and 19 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
theorem Dickson.card_eq_pm_z1_np' line 493 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, Eq, Nat.card, HMul.hMul, Dickson.normalizerQuotient and 2 more
Proof uses: Eq.mpr, HDiv.hDiv, Subgroup.normalizer, id, congrArg, Dickson.normalizerQuotient.eq_1, Nat.mul_div_cancel', Subgroup.card_dvd_of_le, Subgroup.le_normalizer, mul_comm, Eq.symm, Nat.card_eq_fintype_card, HasQuotient.Quotient, Nat.card_congr, Sylow.equivQuotientNormalizer, Subgroup.card_eq_card_quotient_mul_card_subgroup
50 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.branch2_params_of_divisibility line 503 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Not, Dvd.dvd, HSub.hSub, GT.gt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Or, And, Eq
Proof uses: Exists, Exists.intro, Decidable.byContradiction, LE.le, Eq.mpr, eq_of_heq, Dvd, HEq, Eq.refl, HEq.refl, Eq.symm, Int, id, Eq.trans, congr, congrArg, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_sub and 111 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 112 steps
Open to load the checked before-and-after goal states.
theorem Dickson.nonsplit_torus_divides_geo line 583 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, Fintype.card and 4 more
Proof uses: Eq, Quotient, Dickson.PhiType, MulAction.orbitRel, HasEquiv.Equiv, Dickson.num_orbits_eq_two, Not, Set, Dickson.ProjectiveLine, Dickson.Phi, MulAction.orbit, Subtype.mk, Dickson.sylowFixedPoint, Dickson.sylow_fixedPt_mem_Phi, Exists, Decidable.byContradiction, Eq.mpr, False, id, congrArg and 84 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
theorem Dickson.nonsplit_torus_ge_two_arith line 648 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, HMul.hMul, HSub.hSub, HDiv.hDiv
Proof uses: Nat.casesAuxOn, False.elim, Eq, id, LT.lt, Decidable.byContradiction, Not, Eq.mpr, congrArg, Nat.mul_div_cancel_left, GT.gt, Nat.mul_pos, Eq.mp, MulZeroClass.mul_zero, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr and 23 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
theorem Dickson.branch2_params line 673 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, Fintype.card and 9 more
Proof uses: Dickson.sylow_card_ge_3, Nat.div_pos, Subgroup.normalizer, Subgroup.card_le_of_le, Subgroup.le_normalizer, Nat.card_pos, Dickson.normalizer_complement_divides_main, Dickson.card_sylow_mod_card, Not, HPow.hPow, Exists, False, Dickson.sylow_card_prime_pow, Fact.out, Eq.mpr, id, congrArg, Eq.symm, Nat.Prime.eq_one_or_self_of_dvd, Nat.Prime.dvd_of_dvd_pow and 16 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
theorem Dickson.nonsplit_torus_ge_two line 707 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, Fintype.card and 6 more
Proof uses: Dickson.sylow_card_ge_3, Eq, Dickson.card_sylow_mod_card, Nat.casesAuxOn, Decidable.byContradiction, Not, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring and 72 more
146 instances, coercions and auxiliary constants left out.

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

FLT/Slop/PGL2/FiniteSubgroups/PartitionProof.lean

The partition equation for wild finite subgroups of PGL₂(𝔽̄_p)

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

The partition equation for wild finite subgroups of `PGL₂(𝔽̄_p)`