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

40 declarations, 0 contain sorry, 0 declared as axioms

Basic theory of `PGL₂` over the algebraic closure of `𝔽_p`

This file sets up the basic objects used in the proof of Dickson's classification of the finite subgroups of PGL₂(𝔽̄_p) for p an odd prime.

We define the group PGLOf F := PGL₂(F) for a field F (as the quotient of GL₂(F) by its centre) and the projective line ProjectiveLine p := ℙ¹(K p) together with its natural PGLOf (K p)-action, where K p is the algebraic closure of 𝔽_p from FLT.KnownIn1980s.PGL2.Defs. The whole FLT.Slop.PGL2 development is stated in terms of PGLOf (K p), which is definitionally (but not reducibly) equal to the public Dickson.PGL p.

The main results are:

Dickson.pgl_mulEquiv_psl: over the algebraically closed field K p, the natural map PSL₂(K p) → PGL₂(K p) is an isomorphism.
Dickson.exists_finite_subfield_conjugate: every finite subgroup of PGLOf (K p) can be conjugated into the image of PGL₂(F) for some finite subfield F of K p.
Dickson.card_eigenvalues and Dickson.fixedPoints_card: a nontrivial element of PGLOf (K p) fixes either one or two points of the projective line, according to whether its lift to GL₂ has one or two eigenvalues.

Imports (10)

Imported by 8 files

lemma Dickson.Nat.factorization_eq_one line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, Nat.Prime, Not, Dvd.dvd, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, HAdd.hAdd, Nat.factorization_mul, False, dvd_zero, Eq.symm, Nat.Prime.ne_zero, Finsupp.add_apply, Nat.factorization_eq_zero_of_not_dvd, Finsupp.single, Nat.Prime.factorization, Finsupp.single_eq_same, zero_add, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Dickson.Nat.factorization_eq_two line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, Nat.Prime, Not, Dvd.dvd, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, HAdd.hAdd, Nat.factorization_mul, mul_ne_zero, False, dvd_zero, Eq.symm, Nat.Prime.ne_zero, Finsupp.add_apply, Finsupp.single, Nat.Prime.factorization, Finsupp.single_eq_same, Nat.factorization_eq_zero_of_not_dvd, Eq.refl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev Dickson.PGLOf The projective general linear group PGL₂(F) over a field F, i.e. GL₂(F) modulo its centre line 105 source
Source documentation
The projective general linear group PGL₂(F) over a field F, i.e. GL₂(F) modulo its centre. The development in FLT.Slop.PGL2 works with this explicit quotient model throughout; it is definitionally equal to Matrix.ProjGenLinGroup (Fin 2) F (and hence, over F = K p, to the public Dickson.PGL p), but not reducibly so, which is why the proofs below are stated in terms of PGLOf rather than Dickson.PGL.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field
Proof uses: HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Subgroup, Matrix, Subgroup.center
10 instances, coercions and auxiliary constants left out.
```
abbrev PGLOf (F : Type*) [Field F] := GL (Fin 2) F ⧸ Subgroup.center (GL (Fin 2) F)
```
theorem Dickson.pgl_mulEquiv_psl line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Nonempty, MulEquiv, Dickson.PGLOf, Dickson.K, ZMod, Dickson.PSL, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Matrix.SpecialLinearGroup
Proof uses: Exists, Eq, HPow.hPow, Polynomial.IsRoot, HSub.hSub, Polynomial, Polynomial.X, RingHom, Polynomial.C, IsAlgClosed.exists_root, WithBot, Polynomial.degree, False.elim, False, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 85 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
abbrev Dickson.ProjectiveLine The projective line ℙ¹(K p) over K p line 176 source
Source documentation
The projective line ℙ¹(K p) over K p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime
Proof uses: Projectivization, Dickson.K, Fin, OfNat.ofNat, ZMod
11 instances, coercions and auxiliary constants left out.
```
abbrev ProjectiveLine : Type := Projectivization (K p) (Fin 2 → K p)
```
Mentions: Dickson.K
def Dickson.glActionProjectiveLine The natural GL₂(K p)-action on the projective line ℙ¹(K p) line 179 source
Source documentation
The natural GL₂(K p)-action on the projective line ℙ¹(K p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, MulAction, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Dickson.ProjectiveLine, Matrix
39 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
@[reducible] def glActionProjectiveLine : MulAction (GL (Fin 2) (K p)) (ProjectiveLine p) :=
…
```
Mentions: Dickson.K, Dickson.ProjectiveLine
instance Dickson.(instance at line 182) line 182 source
instance Dickson.(instance at line 200) line 200 source
def Dickson.pglMap The group homomorphism PGL₂(F) → PGL₂(L) induced by a ring homomorphism f : F →+* L line 208 source
Source documentation
The group homomorphism PGL₂(F) → PGL₂(L) induced by a ring homomorphism f : F →+* L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, RingHom, MonoidHom, Dickson.PGLOf, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Matrix, Subgroup.center
Proof uses: QuotientGroup.map, Matrix.GeneralLinearGroup.map
29 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
def pglMap {F L : Type*} [Field F] [Field L] (f : F →+* L) : PGLOf F →* PGLOf L :=
…
```
Mentions: Dickson.PGLOf
theorem Dickson.finite_of_closure_finite line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Set, Dickson.K, Set.Finite, Finite, Subtype, Membership.mem, Subfield, ZMod, Subfield.closure
Proof uses: Finset, Eq, Exists, Set.Finite.exists_finset_coe, IntermediateField, IntermediateField.adjoin, Iff.mp, Module.Finite, Module.finite_iff_finite, IntermediateField.finiteDimensional_adjoin, IsAlgebraic, IsIntegral, isAlgebraic_iff_isIntegral, Algebra.IsAlgebraic.isAlgebraic, AlgebraicClosure, Subtype.mk, Iff.mpr, LE.le, Union.union, Set.range and 11 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Dickson.exists_finite_subfield_conjugate line 271 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, Exists, Subfield, LE.le, Subgroup.map, MulAut and 5 more
Proof uses: Eq, HasQuotient.Quotient, Fintype, Fintype.ofFinite, Finset, Finset.image, Finset.univ, Subfield.closure, Set.iUnion, Set.range, Prod, Prod.fst, Prod.snd, Dickson.finite_of_closure_finite, Set.Finite.biUnion, Finset.finite_toSet, Set, Set.finite_range, Subfield.subset_closure, Iff.mpr and 47 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
def Dickson.fixedPoints The set of fixed points of the action of g : PGLOf (K p) on the projective line ℙ¹(K p) line 307 source
Source documentation
The set of fixed points of the action of g : PGLOf (K p) on the projective line ℙ¹(K p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Set, Dickson.ProjectiveLine
Proof uses: Function.fixedPoints, HSMul.hSMul
6 instances, coercions and auxiliary constants left out.
```
def fixedPoints (g : PGLOf (K p)) : Set (ProjectiveLine p) := Function.fixedPoints (fun x ↦ g • x)
…
```
Mentions: Dickson.PGLOf, Dickson.K, Dickson.ProjectiveLine
theorem Dickson.fixedPoints_lift line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Dickson.ProjectiveLine, Iff, Membership.mem, Set, Dickson.fixedPoints, Matrix, Subgroup.center, Exists, Eq, Matrix.mulVec, Projectivization.rep, HSMul.hSMul
Proof uses: Iff.intro, id, Projectivization.mk, Projectivization.rep_nonzero, Projectivization, RingHom.id, MonoidHom, Module.End, DistribMulAction.toModuleEnd, Subtype.mk, Ne, Units, Eq.mp, congrArg, propext, Projectivization.mk_eq_mk_iff, Exists.intro, Eq.symm, Projectivization.mk_rep, Eq.mpr and 12 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
theorem Dickson.card_eigenvalues line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Eq, Set.ncard, Set.ofPred, Matrix.det, HSub.hSub, Matrix, HSMul.hSMul, ite, HPow.hPow, Matrix.trace, HMul.hMul
Proof uses: HAdd.hAdd, Eq.mpr, id, congrArg, Matrix.det_fin_two, Matrix.trace_fin_two, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos and 118 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
theorem Dickson.eigenvectors_linearIndependent line 395 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Ne, Eq, Matrix.mulVec, Matrix, HSMul.hSMul, LinearIndependent, Nat.succ, Matrix.vecCons, Matrix.vecEmpty
Proof uses: Iff.mpr, And, linearIndependent_fin2, And.intro, id, Trans.trans, Eq.symm, Eq.mpr, congrArg, Eq.refl, Matrix.mulVec_smul, SMulCommClass.smul_comm, HSub.hSub, sub_smul, sub_self, Or.resolve_left, Iff.mp, Or, smul_eq_zero, sub_ne_zero
101 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Dickson.eigenvector_isMultiple_of_basis line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Ne, Eq, Matrix.mulVec, Matrix, HSMul.hSMul, Exists, Or
Proof uses: LinearIndependent, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Dickson.eigenvectors_linearIndependent, Finset.sum, Finset.univ, Iff.mp, Membership.mem, Submodule, Submodule.span, Set.range, Submodule.mem_span_range_iff_exists_fun, Eq.rec, Top.top, Submodule.mem_top, Eq.symm, Submodule.eq_top_of_finrank_eq, Eq.mpr, Module.finrank and 64 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
theorem Dickson.fixedPoints_eq_pair line 451 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Ne, Eq, Matrix.mulVec, Matrix, HSMul.hSMul, Set, Dickson.ProjectiveLine, Dickson.fixedPoints, Subgroup.center, Insert.insert, Projectivization, Projectivization.mk and 1 more
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Or, id, congrArg, propext, Set.mem_insert_iff, Set.mem_singleton_iff, Iff.intro, Exists, Projectivization.rep, Dickson.eigenvector_isMultiple_of_basis, Iff.mp, Dickson.fixedPoints_lift, Or.inl, Projectivization.rep_nonzero, Eq.symm, Projectivization.mk_rep and 9 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
theorem Dickson.ncard_fixedPoints_eq_two_of_ne_eigenvalues line 474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Ne, Eq, Matrix.det, HSub.hSub, Matrix, HSMul.hSMul, Set.ncard, Dickson.ProjectiveLine, Dickson.fixedPoints, Subgroup.center
Proof uses: And, Matrix.mulVec, Exists, Iff.mpr, Matrix.exists_mulVec_eq_zero_iff, Eq.mpr, Insert.insert, Projectivization, Set, Projectivization.mk, Singleton.singleton, id, congrArg, Dickson.fixedPoints_eq_pair, Eq.mp, Matrix.one_mulVec, Matrix.smul_mulVec, propext, sub_eq_zero, Matrix.sub_mulVec and 13 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Dickson.ncard_fixedPoints_eq_two_of_discrim_ne_zero line 491 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Ne, HPow.hPow, Matrix.trace, Matrix, HMul.hMul, Matrix.det, Eq, Set.ncard, Dickson.ProjectiveLine, Dickson.fixedPoints, Subgroup.center
Proof uses: Polynomial, HAdd.hAdd, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, id, Eq.mpr, ite, True, congrFun', congrArg, Eq.trans, Polynomial.coeff_add, congr, Polynomial.coeff_sub and 101 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
theorem Dickson.ncard_fixedPoints_eq_one_of_discrim_zero line 543 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Not, Exists, Eq, Matrix, HSMul.hSMul, HPow.hPow, Matrix.trace, HMul.hMul, Matrix.det, Set.ncard, Dickson.ProjectiveLine, Dickson.fixedPoints and 1 more
Proof uses: Set.ofPred, HSub.hSub, Eq.mpr, ite, id, congrArg, Dickson.card_eigenvalues, ite_eq_left, Eq.refl, Set, Singleton.singleton, Iff.mp, Set.ncard_eq_one, Iff, Membership.mem, Iff.rfl, And, Ne, Matrix.mulVec, Iff.mpr and 64 more
179 instances, coercions and auxiliary constants left out.

Tactic trace: 91 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orderOf_coprime_of_discrim_ne_zero line 634 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod, Ne, HPow.hPow, Matrix.trace, Matrix, HMul.hMul, Matrix.det, IsOfFinOrder, HasQuotient.Quotient, Subgroup, Subgroup.center, Nat.Coprime, orderOf
Proof uses: Polynomial, HAdd.hAdd, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, WithBot, Polynomial.degree, Eq, Finsupp, Polynomial.coeff, id, Eq.mpr, ite, True, congrFun', congrArg, Eq.trans, Polynomial.coeff_add, congr and 207 more
266 instances, coercions and auxiliary constants left out.

Tactic trace: 262 steps (first 200 of 262)
Open to load the checked before-and-after goal states.
theorem Dickson.orderOf_eq_prime_of_discrim_zero line 892 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Matrix.GeneralLinearGroup, Fin, Dickson.K, ZMod, Not, Exists, Eq, Matrix, HSMul.hSMul, HPow.hPow, Matrix.trace, HMul.hMul, Matrix.det, orderOf, HasQuotient.Quotient and 2 more
Proof uses: HDiv.hDiv, HSub.hSub, Ne, NeZero.out, NeZero.of_not_dvd, Dvd.dvd, absurd, LE.le, False, Nat.le_of_dvd, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Iff.mpr, LT.lt, not_le, Fact.out, Trans.trans and 142 more
205 instances, coercions and auxiliary constants left out.

Tactic trace: 122 steps
Open to load the checked before-and-after goal states.
theorem Dickson.fixedPoints_dichotomy line 1055 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, Ne, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, IsOfFinOrder, And, Iff, Eq, Set.ncard, Dickson.ProjectiveLine, Dickson.fixedPoints and 2 more
Proof uses: HasQuotient.Quotient, Subgroup, Exists, QuotientGroup.mk_surjective, Not, HSMul.hSMul, False, Eq.mpr, Membership.mem, id, congrArg, propext, QuotientGroup.eq_one_iff, HMul.hMul, Subgroup.mem_center_iff, Units.ext, Matrix.mul_smul, Matrix.smul_mul, Matrix.mul_one, Matrix.one_mul and 21 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
theorem Dickson.fixedPoint_of_center_unique line 1092 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, Eq, HSMul.hSMul
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Eq.symm, SemigroupAction.mul_smul, Iff.mp, Subgroup.mem_center_iff, Eq.refl
61 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Dickson.isPGroup_exists_common_fixedPoint line 1098 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, IsPGroup, Exists, Dickson.ProjectiveLine, Eq and 1 more
Proof uses: dite, Exists.intro, Classical.arbitrary, Eq.mpr, id, congrArg, one_smul, Eq.refl, Not, And, Ne, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, funext, Nontrivial, Nontrivial.mk, Subtype.mk, Iff.mpr, Iff.not and 52 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orderOf_eq_prime_of_prime_pow line 1145 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, GE.ge, Eq, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, HPow.hPow
Proof uses: HasQuotient.Quotient, Subgroup, Exists, QuotientGroup.mk_surjective, Not, HSMul.hSMul, False, Iff.mpr, Membership.mem, QuotientGroup.eq_one_iff, HMul.hMul, Subgroup.mem_center_iff, Units.ext, id, Eq.mpr, congrArg, mul_smul_comm, smul_mul_assoc, mul_one, one_mul and 31 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem Dickson.isPGroup_orderOf_eq_prime line 1167 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, IsPGroup, Ne, Eq, orderOf
Proof uses: HPow.hPow, Exists, And, LE.le, Iff.mp, Dvd.dvd, Nat.dvd_prime_pow, Fact.out, Iff.mpr, orderOf_dvd_iff_pow_eq_one, GE.ge, Nat.pos_of_ne_zero, orderOf_eq_one_iff, Eq.mp, congrArg, pow_zero, Eq.mpr, id, Subgroup.orderOf_coe, Dickson.orderOf_eq_prime_of_prime_pow
62 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Dickson.isPGroup_exponent_dvd_prime line 1184 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, IsPGroup, Dvd.dvd, Monoid.exponent
Proof uses: Monoid.exponent_dvd_of_forall_pow_eq_one, dite, Eq, HPow.hPow, HMul.hMul, Eq.mpr, id, congrArg, one_pow, Eq.refl, Not, orderOf, Eq.symm, Subgroup.orderOf_coe, Dickson.isPGroup_orderOf_eq_prime, pow_orderOf_eq_one, Eq.mp
61 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Dickson.infinity The point ∞ = [1 : 0] of the projective line ℙ¹(K p) line 1199 source
Source documentation
The point ∞ = [1 : 0] of the projective line ℙ¹(K p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.ProjectiveLine
Proof uses: Projectivization.mk, Dickson.K, Fin, OfNat.ofNat, ZMod, Matrix.vecCons, Matrix.vecEmpty
22 instances, coercions and auxiliary constants left out.
```
def infinity : ProjectiveLine p := Projectivization.mk (K p) ![1,
…
```
Mentions: Dickson.ProjectiveLine, Dickson.K
theorem Dickson.fixesInfinity_iff_upperTriangular line 1203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Iff, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, Exists, Ne, HMul.hMul, OfNat.ofNat, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero and 4 more
Proof uses: Nat.succ, one_ne_zero, congr_fun, Iff.intro, HasQuotient.Quotient, Subgroup, QuotientGroup.mk_surjective, Matrix.det, Matrix.det_ne_zero_of_left_inverse, Inv.inv, Units, Units.inv_mul, Matrix.mulVec, Iff.mp, And, Matrix.exists_mulVec_eq_zero_iff, Exists.intro, And.intro, id, Projectivization and 58 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
theorem Dickson.upper_triangular_ratio_unique line 1255 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Ne, HMul.hMul, ZMod, OfNat.ofNat, Eq, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty and 1 more
Proof uses: Eq.mpr, Matrix.det, HSub.hSub, id, congrArg, Matrix.det_fin_two, MulZeroClass.mul_zero, sub_zero, RingHom, Matrix.scalar, Membership.mem, Set, Set.range, Iff.mp, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, QuotientGroup.eq, Units, Eq.symm, Units.val_mul, mul_inv_cancel_left and 36 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
theorem Dickson.upper_triangular_mul_ratio line 1291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Ne, HMul.hMul, ZMod, OfNat.ofNat, Eq, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty and 1 more
Proof uses: congr_arg, Units.ext, Matrix.ext, id, Eq.mpr, Finset.sum, Finset.univ, congrArg, Matrix.mul_apply, Fin.sum_univ_two, Unit, MulZeroClass.mul_zero, add_zero, Eq.refl, MulZeroClass.zero_mul, zero_add
81 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Dickson.ratio_one_imp_unipotent line 1310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.K, Ne, HMul.hMul, ZMod, Eq, Inv.inv, Or, orderOf, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero and 4 more
Proof uses: Eq.mpr, id, congrArg, MulZeroClass.zero_mul, Eq.refl, eq_of_div_eq_one, Matrix.det, HSub.hSub, Matrix.det_fin_two, MulZeroClass.mul_zero, sub_zero, mul_one, one_ne_zero, Membership.mem, propext, QuotientGroup.eq, Set, Set.range, RingHom, Matrix.scalar and 81 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
theorem Dickson.isUnipotent_of_fixesInfinity_orderOf line 1354 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, Exists, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv and 3 more
Proof uses: Ne, HMul.hMul, Iff.mp, Dickson.fixesInfinity_iff_upperTriangular, dite, Exists.intro, HDiv.hDiv, Eq.mpr, id, congrArg, Eq.symm, Membership.mem, Subgroup, Inv.inv, HasQuotient.Quotient, propext, QuotientGroup.eq, Units.ext, Matrix.det, HSub.hSub and 113 more
170 instances, coercions and auxiliary constants left out.

Tactic trace: 69 steps
Open to load the checked before-and-after goal states.
theorem Dickson.exists_smul_eq_infinity line 1434 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.ProjectiveLine, Exists, Dickson.PGLOf, Dickson.K, ZMod, Eq, HSMul.hSMul, Dickson.infinity
Proof uses: Fin, OfNat.ofNat, Projectivization.rep, Matrix, And, Ne, Matrix.det, Matrix.mulVec, Matrix.vecCons, Nat.succ, Matrix.vecEmpty, dite, Projectivization.rep_nonzero, funext, Unit, Exists.intro, Equiv, Matrix.of, Inv.inv, And.intro and 48 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
theorem Dickson.commute_of_orderOf_prime_fixesInfinity line 1474 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, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, HMul.hMul
Proof uses: Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Exists, Dickson.isUnipotent_of_fixesInfinity_orderOf, Eq.mpr, id, congrArg, Group, Subgroup, Eq.rec, HasQuotient.Quotient, Eq.refl, Units.ext, Matrix.ext, Finset.sum, Finset.univ, Matrix.mul_apply and 29 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
theorem Dickson.commute_of_orderOf_prime_common_fixedPoint line 1494 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, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, HSMul.hSMul, HMul.hMul
Proof uses: Dickson.infinity, Exists, Dickson.exists_smul_eq_infinity, Inv.inv, SemiconjBy.orderOf_eq, SemiconjBy, id, of_eq_true, Eq.trans, HPow.hPow, Int, Neg.neg, True, congr, congrArg, congrFun', HAdd.hAdd, neg_add_cancel, zpow_zero, one_mul and 9 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Dickson.isPGroup_comm_exponent_fixedPoint line 1511 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, IsPGroup, Nontrivial, And, Eq and 6 more
Proof uses: Exists, Dickson.isPGroup_exists_common_fixedPoint, And.intro, Subtype.ext, dite, Eq.mpr, id, congrArg, one_mul, mul_one, Eq.refl, Not, Dickson.commute_of_orderOf_prime_common_fixedPoint, Dickson.isPGroup_orderOf_eq_prime, Subtype.prop, Dickson.isPGroup_exponent_dvd_prime, Exists.intro, Ne, exists_ne, orderOf and 24 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem Dickson.card_center_GL2 line 1548 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Fintype, Eq, Nat, Nat.card, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Membership.mem, Subgroup, Matrix, Subgroup.center, HSub.hSub, Fintype.card
Proof uses: Iff, Exists, And, Ne, Matrix.diagonal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Iff.intro, Matrix.det, HMul.hMul, congrArg, Units, Matrix.GeneralLinearGroup.mkOfDetNeZero, Eq.symm, Iff.mp, Subgroup.mem_center_iff, Equiv, Matrix.of, congrFun and 53 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 81 steps
Open to load the checked before-and-after goal states.
theorem Dickson.card_PGL2 line 1643 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Fintype, Eq, Nat, Nat.card, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Subgroup, Matrix, Subgroup.center, HMul.hMul, Fintype.card, HSub.hSub, HPow.hPow
Proof uses: mul_right_cancel₀, Nat.sub_ne_zero_of_lt, Fintype.one_lt_card, Eq.mpr, Subtype, Membership.mem, id, congrArg, Eq.symm, Dickson.card_center_GL2, Subgroup.card_eq_card_quotient_mul_card_subgroup, Finset.prod, Finset.univ, Matrix.card_GL_field, Fin.prod_univ_two, Fin.val_zero, HAdd.hAdd, Fin.val_one, pow_zero, pow_one and 6 more
66 instances, coercions and auxiliary constants left out.

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

FLT/Slop/PGL2/FiniteSubgroups/PGLBasic.lean

Basic theory of PGL₂ over the algebraic closure of 𝔽_p

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

Basic theory of `PGL₂` over the algebraic closure of `𝔽_p`