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

96 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing a finite field from a wild subgroup of `PGL₂(𝔽̄_p)`

Let G be a finite subgroup of PGLOf (K p) = PGL₂(𝔽̄_p) whose Sylow p-subgroup is not cyclic of order dividing p. This file reconstructs a finite subfield 𝔽_q ⊆ 𝔽̄_p (q = p^m) from the translations contained in G.

We define:

Dickson.FqInK p m: the subfield {x | x ^ p ^ m = x} of K p = 𝔽̄_p, i.e. the image of the Galois field 𝔽_{p^m};
Dickson.translationPGL and Dickson.dilationPGL: the upper-triangular translation x ↦ x + b and dilation x ↦ cx as elements of PGLOf (K p);
Dickson.translationSet H: the set of b with x ↦ x + b in H;
Dickson.galoisFieldRingHom: an embedding GaloisField p m →+* K p with image FqInK p m.

The main results identify the translation set of (a conjugate of) the subgroup fixing ∞ with the additive group of 𝔽_{p^m}, the first step in recognising G as PSL₂(𝔽_q) or PGL₂(𝔽_q).

Imports (2)

Imported by 2 files

def Dickson.FqInK The subfield 𝔽_{p^m} sitting inside K p = 𝔽̄_p, i.e. the set of x with x ^ (p ^ m) = x line 57 source
Source documentation
The subfield 𝔽_{p^m} sitting inside K p = 𝔽̄_p, i.e. the set of x with x ^ (p ^ m) = x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Set, Dickson.K
Proof uses: Set.ofPred, Eq, HPow.hPow, ZMod
10 instances, coercions and auxiliary constants left out.
```
noncomputable def FqInK (m : ℕ) : Set (K p) :=
…
```
Mentions: Dickson.K
theorem Dickson.F_q_add_closed line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Membership.mem, Set, Dickson.FqInK, HAdd.hAdd, ZMod
Proof uses: id, Eq.mpr, Eq, HPow.hPow, congrArg, add_pow_char_pow, Eq.refl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.F_q_mul_closed line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Membership.mem, Set, Dickson.FqInK, HMul.hMul, ZMod
Proof uses: id, Eq.mpr, Eq, HPow.hPow, congrArg, mul_pow, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.F_q_zero line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Membership.mem, Dickson.K, Set, Dickson.FqInK, OfNat.ofNat, ZMod
Proof uses: zero_pow, HPow.hPow, pow_ne_zero, Nat.Prime.ne_zero, Fact.out
30 instances, coercions and auxiliary constants left out.
theorem Dickson.F_q_one line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Membership.mem, Dickson.K, Set, Dickson.FqInK, OfNat.ofNat, ZMod
Proof uses: one_pow, HPow.hPow
19 instances, coercions and auxiliary constants left out.
theorem Dickson.F_q_card line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Eq, Set.ncard, Dickson.K, Dickson.FqInK, HPow.hPow
Proof uses: Polynomial, ZMod, HSub.hSub, Polynomial.X, Polynomial.natDegree, Eq.trans, Polynomial.natDegree_sub_eq_left_of_natDegree_lt, Eq.mpr, LT.lt, id, congrArg, Polynomial.natDegree_X_pow, Polynomial.natDegree_X, one_lt_pow₀, Nat.Prime.one_lt, Fact.out, Ne, ne_of_apply_ne, Polynomial.natDegree_zero, ne_of_gt and 105 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Dickson.additive_subgroup_eq_F_q line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Set, Dickson.K, Eq, Set.ncard, HPow.hPow, Membership.mem, ZMod, HSub.hSub, Ne, HMul.hMul, Dickson.FqInK
Proof uses: LE.le, Or, eq_or_ne, Eq.symm, Eq.rec, mul_left_cancel₀, Eq.mpr, HAdd.hAdd, id, congrArg, pow_succ', Nat.sub_add_cancel, Nat.one_le_pow, Nat.Prime.pos, Fact.out, mul_one, Eq.refl, Set.eq_of_subset_of_ncard_le, Eq.le, Eq.trans and 4 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Dickson.translationGL The translation x ↦ x + b as the element !![1, b; 0, 1] of GL₂(K p) line 125 source
Source documentation
The translation x ↦ x + b as the element !![1, b; 0, 1] of GL₂(K p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, ZMod
Proof uses: Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix, Matrix.of, Matrix.vecCons, Matrix.vecEmpty
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def translationGL (b : K p) : GL (Fin 2) (K p) :=
…
```
Mentions: Dickson.K
def Dickson.dilationGL The dilation x ↦ c x (for c ≠ 0) as the element !![c, 0; 0, 1] of GL₂(K p) line 130 source
Source documentation
The dilation x ↦ c x (for c ≠ 0) as the element !![c, 0; 0, 1] of GL₂(K p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Ne, OfNat.ofNat, ZMod, Matrix.GeneralLinearGroup, Fin
Proof uses: Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix, Matrix.of, Matrix.vecCons, Matrix.vecEmpty
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def dilationGL (c : K p) (hc : c ≠ 0) : GL (Fin 2) (K p) :=
…
```
Mentions: Dickson.K
def Dickson.translationPGL The translation x ↦ x + b as an element of PGLOf (K p) = PGL₂(𝔽̄_p) line 135 source
Source documentation
The translation x ↦ x + b as an element of PGLOf (K p) = PGL₂(𝔽̄_p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Dickson.PGLOf, ZMod
Proof uses: Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.translationGL
14 instances, coercions and auxiliary constants left out.
```
noncomputable def translationPGL (b : K p) : PGLOf (K p) :=
…
```
Mentions: Dickson.K, Dickson.PGLOf
def Dickson.dilationPGL The dilation x ↦ c x (for c ≠ 0) as an element of PGLOf (K p) = PGL₂(𝔽̄_p) line 140 source
Source documentation
The dilation x ↦ c x (for c ≠ 0) as an element of PGLOf (K p) = PGL₂(𝔽̄_p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Ne, OfNat.ofNat, ZMod, Dickson.PGLOf
Proof uses: Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Dickson.dilationGL
23 instances, coercions and auxiliary constants left out.
```
noncomputable def dilationPGL (c : K p) (hc : c ≠ 0) : PGLOf (K p) :=
…
```
Mentions: Dickson.K, Dickson.PGLOf
theorem Dickson.translationPGL_zero line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Eq, Dickson.PGLOf, Dickson.K, ZMod, Dickson.translationPGL, OfNat.ofNat, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center
Proof uses: id, Group, Subgroup, Eq.rec, HasQuotient.Quotient, Eq.refl, Dickson.translationGL, Units.ext, Matrix.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk and 9 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translationPGL_mul line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Eq, Dickson.PGLOf, ZMod, HMul.hMul, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.translationPGL, HAdd.hAdd
Proof uses: id, Group, Subgroup, Eq.rec, HasQuotient.Quotient, Eq.refl, Dickson.translationGL, Units.ext, Matrix.ext, Eq.mpr, congrArg, Units, Units.val_mul, Finset.sum, Finset.univ, Matrix.mul_apply, Fin.sum_univ_two, Unit, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 24 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translationPGL_inv line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Eq, Dickson.PGLOf, ZMod, Inv.inv, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.translationPGL, Neg.neg
Proof uses: inv_eq_of_mul_eq_one_right, Eq.mpr, HMul.hMul, HAdd.hAdd, id, congrArg, Dickson.translationPGL_mul, add_neg_cancel, Dickson.translationPGL_zero, Eq.refl
74 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Dickson.order_p_fixing_infinity_is_translation line 170 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, And, Ne and 1 more
Proof uses: Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Dickson.isUnipotent_of_fixesInfinity_orderOf, False, id, ne_of_gt, lt_trans, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Fact.out, LT.lt, Eq.symm, Eq.mp, congrArg and 4 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Dickson.n_p_gt_one_of_pgl_order line 181 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 5 more
Proof uses: Decidable.byContradiction, Not, Exists, False, Iff.mp, Fintype.card_eq_one_iff, le_antisymm, LT.lt, LE.le, not_lt, Fintype.card_pos, Dvd.dvd, Subgroup.normalizer, Top.top, Iff.mpr, Subgroup.eq_top_iff', Eq.mpr, id, congrArg, Set and 29 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem Dickson.z1_eq_pm_minus_one line 204 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: Subgroup.normalizer, Nat.eq_of_mul_eq_mul_left, Nat.succ, Nat.succ_pos, Trans.trans, HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, Dickson.n_p_eq_pgl, Nat.card_eq_fintype_card, HasQuotient.Quotient, Nat.card_congr, Sylow.equivQuotientNormalizer, Subgroup.card_eq_card_quotient_mul_card_subgroup, Nat.mul_comm, Nat.pow_mul, Nat.one_pow, Nat.sq_sub_sq and 9 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Dickson.translationSet The set of b : K p for which the translation x ↦ x + b lies in the subgroup H line 222 source
Source documentation
The set of b : K p for which the translation x ↦ x + b lies in the subgroup H.

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
Proof uses: Set.ofPred, Membership.mem, Dickson.translationPGL
28 instances, coercions and auxiliary constants left out.
```
noncomputable def translationSet (H : Subgroup (PGLOf (K p))) : Set (K p) :=
…
```
Mentions: Dickson.PGLOf, Dickson.K
theorem Dickson.p_subgroup_fixing_infinity_translations line 225 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, Eq, Dickson.ProjectiveLine and 8 more
Proof uses: dite, HMul.hMul, Exists.intro, Eq.trans, Eq.symm, Dickson.translationPGL_zero, Not, Exists.imp, Ne, And.right, Dickson.order_p_fixing_infinity_is_translation, Dickson.isPGroup_orderOf_eq_prime, Subtype.mk, congrArg, Set, Set.image, Set.ext, Iff.intro, Eq.rec, And.intro and 79 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translationSet_zero line 260 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, Membership.mem, Set, Dickson.translationSet
Proof uses: Dickson.translationPGL, Eq.rec, Eq, Subgroup.one_mem, Eq.symm, Dickson.translationPGL_zero
40 instances, coercions and auxiliary constants left out.
theorem Dickson.translationSet_add line 265 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, Membership.mem, Set, Dickson.translationSet, HAdd.hAdd
Proof uses: Dickson.translationPGL, Eq.rec, HMul.hMul, Eq, Subgroup.mul_mem, Dickson.translationPGL_mul
42 instances, coercions and auxiliary constants left out.
theorem Dickson.translationSet_neg 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, Membership.mem, Set, Dickson.translationSet, Neg.neg
Proof uses: Dickson.translationPGL, Eq.rec, Inv.inv, Eq, Subgroup.inv_mem, Dickson.translationPGL_inv
50 instances, coercions and auxiliary constants left out.
theorem Dickson.pglMap_injective line 276 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, RingHom, Function.Injective, Dickson.PGLOf, MonoidHom, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Matrix, Subgroup.center, Dickson.pglMap
Proof uses: Eq, HasQuotient.Quotient, Subgroup, Exists, QuotientGroup.mk_surjective, Eq.mpr, Membership.mem, HMul.hMul, Inv.inv, id, congrArg, propext, QuotientGroup.eq, Subgroup.mem_center_iff, Matrix.GeneralLinearGroup.map, Eq.mp, Units.ext, Matrix.ext, congr_arg, congr and 2 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Dickson.galoisFieldRingHom A ring embedding GaloisField p m →+* K p of 𝔽_{p^m} into 𝔽̄_p, with image FqInK p m line 294 source
Source documentation
A ring embedding GaloisField p m →+* K p of 𝔽_{p^m} into 𝔽̄_p, with image FqInK p m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, RingHom, GaloisField, Dickson.K, ZMod
Proof uses: AlgHom.toRingHom, IsAlgClosed.lift
25 instances, coercions and auxiliary constants left out.
```
noncomputable def galoisFieldRingHom (m : ℕ) : GaloisField p m →+* K p :=
…
```
Mentions: Dickson.K
theorem Dickson.galoisFieldRingHom_range_eq_F_q line 301 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Eq, Set, Dickson.K, Set.range, GaloisField, RingHom, ZMod, Dickson.galoisFieldRingHom, Dickson.FqInK
Proof uses: Set.eq_of_subset_of_ncard_le, Membership.mem, HPow.hPow, Eq.mpr, Fintype.card, Dickson.instFintypeGaloisField, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HPow, Eq.trans, Nat.card, Fintype.card_eq_nat_card, GaloisField.card, ne_of_gt, FiniteField.pow_card, map_pow and 15 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translationPGL_in_range line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Dickson.K, Membership.mem, Set, Dickson.FqInK, Dickson.PGLOf, ZMod, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, MonoidHom.range, GaloisField, Dickson.pglMap, Dickson.galoisFieldRingHom and 1 more
Proof uses: Eq, RingHom, Exists, Iff.mp, Set.range, Set.mem_range, Eq.rec, Eq.symm, Dickson.galoisFieldRingHom_range_eq_F_q, Exists.intro, MonoidHom, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Eq.mpr, Ne, Matrix.det, HSub.hSub and 20 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilationPGL_in_range line 336 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Dickson.K, Ne, ZMod, Membership.mem, Set, Dickson.FqInK, Dickson.PGLOf, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, MonoidHom.range, GaloisField, Dickson.pglMap and 2 more
Proof uses: Eq, RingHom, Exists, Iff.mp, Set.range, Set.mem_range, Eq.rec, Eq.symm, Dickson.galoisFieldRingHom_range_eq_F_q, Exists.intro, MonoidHom, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Eq.mpr, Matrix.det, HSub.hSub, HMul.hMul and 18 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Dickson.upper_triangular_in_pgl_range line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Dickson.K, Ne, ZMod, Membership.mem, Set, Dickson.FqInK, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, Subgroup.center, Dickson.PGLOf, MonoidHom.range, GaloisField and 7 more
Proof uses: Eq, Eq.mpr, Matrix.det, HSub.hSub, HMul.hMul, id, congrArg, Matrix.det_fin_two, mul_one, MulZeroClass.mul_zero, sub_zero, Dickson.dilationGL, Dickson.translationGL, HDiv.hDiv, Units.ext, Matrix.ext, Units, Units.val_mul, Finset.sum, Finset.univ and 19 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
def Dickson.P1point The point [c : 1] of the projective line ℙ¹(𝔽̄_p) associated to c : K p line 386 source
Source documentation
The point [c : 1] of the projective line ℙ¹(𝔽̄_p) associated to c : K p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Dickson.ProjectiveLine
Proof uses: Projectivization.mk, Fin, OfNat.ofNat, ZMod, Matrix.vecCons, Matrix.vecEmpty
16 instances, coercions and auxiliary constants left out.
```
noncomputable def P1point (c : K p) : ProjectiveLine p :=
…
```
Mentions: Dickson.K, Dickson.ProjectiveLine
theorem Dickson.fixes_zero_upper_triangular line 390 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, Dickson.ProjectiveLine, HSMul.hSMul, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of and 3 more
Proof uses: Units, Exists, Eq.mp, Projectivization, Projectivization.mk, Iff.mpr, smul_ne_zero_iff_ne, congrArg, propext, Projectivization.mk_eq_mk_iff, Projectivization.smul_mk, Dickson.P1point.eq_1, Matrix.mulVec, congr_fun, Eq.symm, congr, MulZeroClass.mul_zero, Eq.trans, Finset.sum, Finset.univ and 4 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Dickson.fixes_one_diagonal line 403 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, Dickson.ProjectiveLine, HSMul.hSMul, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of and 3 more
Proof uses: Units, Exists, Eq.mp, Projectivization, Projectivization.mk, Iff.mpr, smul_ne_zero_iff_ne, congrArg, propext, Projectivization.mk_eq_mk_iff, Projectivization.smul_mk, Dickson.P1point.eq_1, Matrix.mulVec, congr_fun, Eq.trans, Eq.symm, congr, mul_one, Finset.sum, Finset.univ and 19 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Dickson.pgl_fixes_three_points_eq_one line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, Dickson.P1point, OfNat.ofNat, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center
Proof uses: Exists, Ne, HMul.hMul, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Iff.mp, Dickson.fixesInfinity_iff_upperTriangular, Dickson.fixes_zero_upper_triangular, Dickson.fixes_one_diagonal, Eq.symm
66 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Dickson.upper_triangular_normalizes_translations line 446 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, Dickson.PGLOf, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons and 4 more
Proof uses: Eq.mpr, id, congrArg, propext, mul_inv_eq_iff_eq_mul, Dickson.translationGL, Dickson.translationPGL.eq_1, Dickson.translationGL.eq_1, congr_arg, Units.ext, Matrix.ext, Unit, of_eq_true, Eq.trans, True, congr, Finset.sum, Finset.univ, HAdd.hAdd, Fin.sum_univ_two and 13 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
theorem Dickson.general_matrix_in_pgl_range line 473 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Dickson.K, Ne, HSub.hSub, ZMod, HMul.hMul, Membership.mem, Set, Dickson.FqInK, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, Subgroup, Matrix, Subgroup.center, Dickson.PGLOf and 9 more
Proof uses: Eq, RingHom, Exists, Iff.mp, Set.range, Set.mem_range, Eq.rec, Eq.symm, Dickson.galoisFieldRingHom_range_eq_F_q, Exists.intro, MonoidHom, Eq.mpr, Matrix.det, id, congrArg, Matrix.det_fin_two, map_mul, map_sub, map_zero, congr_arg and 4 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def Dickson.P1Fq The copy of ℙ¹(𝔽_q) (q = p^m) inside the projective line: ∞ together with the points [c : 1] for c ∈ 𝔽_{p^m} line 500 source
Source documentation
The copy of ℙ¹(𝔽_q) (q = p^m) inside the projective line: ∞ together with the points [c : 1] for c ∈ 𝔽_{p^m}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Set, Dickson.ProjectiveLine
Proof uses: Union.union, Singleton.singleton, Dickson.infinity, Set.image, Dickson.K, Dickson.P1point, Dickson.FqInK
2 instances, coercions and auxiliary constants left out.
```
noncomputable def P1Fq (m : ℕ) : Set (ProjectiveLine p) :=
…
```
Mentions: Dickson.ProjectiveLine
theorem Dickson.infinity_mem_P1_Fq line 504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Membership.mem, Dickson.ProjectiveLine, Set, Dickson.P1Fq, Dickson.infinity
Proof uses: Set.mem_union_left, Singleton.singleton, Set.image, Dickson.K, Dickson.P1point, Dickson.FqInK, rfl
2 instances, coercions and auxiliary constants left out.
theorem Dickson.P1point_mem_P1_Fq line 508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Membership.mem, Set, Dickson.FqInK, Dickson.ProjectiveLine, Dickson.P1Fq, Dickson.P1point
Proof uses: Set.mem_union_right, Set.image, Singleton.singleton, Dickson.infinity, Exists.intro, And, Eq, And.intro, rfl
3 instances, coercions and auxiliary constants left out.
theorem Dickson.F_q_neg line 512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.K, Membership.mem, Set, Dickson.FqInK, Neg.neg, ZMod
Proof uses: id, Eq.mpr, Eq, HPow.hPow, HMul.hMul, congrArg, neg_pow, Odd.neg_one_pow, Odd.pow, Nat.Prime.odd_of_ne_two, Fact.out, ne_of_gt, LT.lt, neg_one_mul, Eq.refl
54 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Dickson.F_q_sub_closed line 516 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.K, Membership.mem, Set, Dickson.FqInK, HSub.hSub, ZMod
Proof uses: Eq.rec, HAdd.hAdd, Neg.neg, Eq, Dickson.F_q_add_closed, Dickson.F_q_neg, Eq.symm, sub_eq_add_neg
36 instances, coercions and auxiliary constants left out.
theorem Dickson.three_transitive_case1 line 520 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, Dickson.K, Membership.mem, Set, Dickson.FqInK, Ne, Exists, Dickson.PGLOf, ZMod, And, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center and 9 more
Proof uses: HSub.hSub, HMul.hMul, Eq.mpr, id, congrArg, mul_one, MulZeroClass.mul_zero, sub_zero, Iff.mpr, sub_ne_zero, Ne.symm, Exists.intro, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Matrix.det, Matrix.det_fin_two, And.intro and 28 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
theorem Dickson.three_transitive_case2 line 551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, Dickson.K, Membership.mem, Set, Dickson.FqInK, Ne, Exists, Dickson.PGLOf, ZMod, And, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center and 9 more
Proof uses: HSub.hSub, HMul.hMul, Eq.mpr, id, congrArg, MulZeroClass.mul_zero, mul_one, Neg.neg, zero_sub, propext, neg_ne_zero, Iff.mpr, sub_ne_zero, Ne.symm, Exists.intro, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty and 62 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
theorem Dickson.three_transitive_case3 line 588 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, Dickson.K, Membership.mem, Set, Dickson.FqInK, Ne, Exists, Dickson.PGLOf, ZMod, And, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center and 9 more
Proof uses: HSub.hSub, HMul.hMul, Neg.neg, Eq.mpr, id, congrArg, mul_neg_one, mul_one, HAdd.hAdd, sub_neg_eq_add, add_comm, Eq.symm, sub_eq_add_neg, Iff.mpr, sub_ne_zero, Ne.symm, Exists.intro, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of and 76 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
theorem Dickson.three_transitive_case4 line 625 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, Dickson.K, Membership.mem, Set, Dickson.FqInK, Ne, Exists, Dickson.PGLOf, ZMod, And, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center and 9 more
Proof uses: HSub.hSub, HMul.hMul, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl and 73 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
theorem Dickson.pgl_Fq_three_transitive line 670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, Dickson.ProjectiveLine, Membership.mem, Set, Dickson.P1Fq, Ne, Exists, Dickson.PGLOf, Dickson.K, ZMod, And, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix and 9 more
Proof uses: Dickson.FqInK, Or, Eq.mp, Eq.trans, Union.union, Singleton.singleton, Set.image, congr, congrArg, absurd, rfl, Eq.symm, Dickson.three_transitive_case1, Dickson.three_transitive_case2, Dickson.three_transitive_case3, Dickson.three_transitive_case4
69 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Dickson.preserves_P1Fq_in_range line 692 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, GE.ge, Dickson.PGLOf, Dickson.K, ZMod, Dickson.ProjectiveLine, Membership.mem, Set, Dickson.P1Fq, HSMul.hSMul, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, MonoidHom.range and 3 more
Proof uses: Ne, Dickson.infinity, Dickson.P1point, Eq, Units, Matrix.vecCons, Matrix.vecEmpty, Exists, False, Eq.mp, Projectivization, Projectivization.mk, congrArg, propext, Projectivization.mk_eq_mk_iff, Dickson.P1point.eq_1, Dickson.infinity.eq_1, HMul.hMul, congr_fun, Units.ne_zero and 31 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translation_smul_P1point line 725 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.PGLOf, ZMod, Dickson.translationPGL, Dickson.P1point, HAdd.hAdd
Proof uses: Eq.mpr, Projectivization.mk, Fin, OfNat.ofNat, Matrix.GeneralLinearGroup, Matrix, Dickson.translationGL, Matrix.vecCons, Matrix.vecEmpty, Iff.mpr, Ne, smul_ne_zero_iff_ne, id, congrArg, Projectivization, Projectivization.smul_mk, Exists, Units, propext, Projectivization.mk_eq_mk_iff and 35 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translation_smul_infinity line 738 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.PGLOf, ZMod, Dickson.translationPGL, Dickson.infinity
Proof uses: Iff.mpr, Exists, Ne, HMul.hMul, OfNat.ofNat, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Dickson.fixesInfinity_iff_upperTriangular, Exists.intro, of_eq_true, Eq.trans, True, congrFun' and 14 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilation_smul_P1point line 743 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Ne, OfNat.ofNat, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.PGLOf, Dickson.dilationPGL, Dickson.P1point, HMul.hMul
Proof uses: Eq.mpr, Projectivization.mk, Fin, Matrix.GeneralLinearGroup, Matrix, Dickson.dilationGL, Matrix.vecCons, Matrix.vecEmpty, Iff.mpr, smul_ne_zero_iff_ne, id, congrArg, Projectivization, Projectivization.smul_mk, Exists, Units, propext, Projectivization.mk_eq_mk_iff, Exists.intro, funext and 32 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilation_smul_infinity line 756 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Ne, OfNat.ofNat, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.PGLOf, Dickson.dilationPGL, Dickson.infinity
Proof uses: Iff.mpr, Exists, HMul.hMul, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Dickson.fixesInfinity_iff_upperTriangular, Exists.intro, Eq.mpr, id, congrArg, mul_one, rfl
45 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.F_q_inv line 761 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Membership.mem, Set, Dickson.FqInK, Ne, OfNat.ofNat, ZMod, Inv.inv
Proof uses: Eq.trans, HPow.hPow, inv_pow, congrArg
36 instances, coercions and auxiliary constants left out.
theorem Dickson.F_q_div line 766 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.K, Membership.mem, Set, Dickson.FqInK, Ne, OfNat.ofNat, ZMod, HDiv.hDiv
Proof uses: Eq.mpr, HMul.hMul, Inv.inv, id, Eq, congrArg, div_eq_mul_inv, Dickson.F_q_mul_closed, Dickson.F_q_inv
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Dickson.range_preserves_P1Fq line 773 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Membership.mem, Subgroup, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, MonoidHom.range, GaloisField, Dickson.pglMap, Dickson.galoisFieldRingHom, Dickson.ProjectiveLine, Set and 2 more
Proof uses: Eq, MonoidHom, Quot.ind, QuotientGroup.leftRel, Quot.mk, Eq.mpr, Or, Dickson.infinity, Exists, And, Dickson.FqInK, Dickson.P1point, id, Eq.trans, Union.union, Singleton.singleton, Set.image, congr, congrArg, Eq.mp and 108 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 117 steps
Open to load the checked before-and-after goal states.
theorem Dickson.unique_sylow_fixing_infinity line 889 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.map and 5 more
Proof uses: Dickson.sylow_fixedPoint_injective, Eq.trans, Dickson.sylowFixedPoint, Eq.symm, Dickson.eq_sylow_fixedPoint, Subgroup.mem_map_of_mem
43 instances, coercions and auxiliary constants left out.
theorem Dickson.fixes_infinity_normalizes_sylow line 900 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.map and 6 more
Proof uses: Eq.mpr, id, congrArg, Set, Sylow.coe_coe, Eq.symm, propext, Sylow.smul_eq_iff_mem_normalizer, Dickson.unique_sylow_fixing_infinity, And, MonoidHom, Exists, Iff.mp, Subgroup.mem_map, MulAut, Monoid.End, MulDistribMulAction.toMonoidEnd, MulAut.conj, HMul.hMul, Inv.inv and 7 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Dickson.orbitInfty The orbit of ∞ under the subgroup G', i.e. the set of points g • ∞ for g ∈ G' line 917 source
Source documentation
The orbit of ∞ under the subgroup G', i.e. the set of points g • ∞ for g ∈ 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.ofPred, Exists, And, Membership.mem, Eq, HSMul.hSMul, Dickson.infinity
30 instances, coercions and auxiliary constants left out.
```
def orbitInfty (G' : Subgroup (PGLOf (K p))) : Set (ProjectiveLine p) :=
…
```
Mentions: Dickson.PGLOf, Dickson.K, Dickson.ProjectiveLine
theorem Dickson.preserves_orbitInfty line 922 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, Membership.mem, Dickson.ProjectiveLine, Set, Dickson.orbitInfty, HSMul.hSMul
Proof uses: Eq, Dickson.infinity, Exists.intro, And, HMul.hMul, And.intro, Subgroup.mul_mem, Eq.mpr, id, congrArg, SemigroupAction.mul_smul, Eq.refl
49 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Dickson.infty_mem_orbitInfty line 931 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, Membership.mem, Dickson.ProjectiveLine, Set, Dickson.orbitInfty, Dickson.infinity
Proof uses: Exists.intro, And, Eq, HSMul.hSMul, And.intro, Subgroup.one_mem, one_smul
40 instances, coercions and auxiliary constants left out.
theorem Dickson.orbit_closed_under_translation line 936 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, Membership.mem, Dickson.ProjectiveLine, Set, Dickson.orbitInfty, Dickson.P1point, Dickson.translationPGL, HAdd.hAdd
Proof uses: Eq.rec, HSMul.hSMul, Eq, Dickson.preserves_orbitInfty, Dickson.translation_smul_P1point
40 instances, coercions and auxiliary constants left out.
theorem Dickson.translationSet_scaled_eq_Fq line 944 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GE.ge, OfNat.ofNat, Set, Dickson.K, Eq, Set.ncard, HPow.hPow, Membership.mem, HAdd.hAdd, ZMod, Neg.neg, HSub.hSub, Ne, HMul.hMul, Set.image, Inv.inv, Dickson.FqInK
Proof uses: Dickson.additive_subgroup_eq_F_q, Eq.mpr, id, congrArg, Set.ncard_image_of_injective, Eq.symm, one_mul, mul_inv_cancel₀, mul_assoc, Eq.refl, Exists.intro, And, And.intro, MulZeroClass.mul_zero, inv_mul_cancel₀, mul_left_comm
105 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbitInfty_conj_of_fixes_infty line 964 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, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, Set, Dickson.orbitInfty, Subgroup.map, MulEquiv.toMonoidHom and 4 more
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, id, congrArg, Set.ofPred, Inv.inv, Iff.mpr, inv_smul_eq_iff, Eq.symm, Iff.intro, Iff.mp, Subgroup.mem_map, Exists.intro, And.intro, rfl, HMul.hMul and 3 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
theorem Dickson.projLine_cases line 987 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.ProjectiveLine, Or, Eq, Dickson.infinity, Exists, Dickson.K, Dickson.P1point
Proof uses: Quot.ind, Subtype, Fin, OfNat.ofNat, Ne, ZMod, projectivizationSetoid, Quot.mk, dite, Subtype.mk, Or.inl, funext, Unit, Quotient.sound, Matrix.vecCons, Matrix.vecEmpty, Exists.intro, Units, HSMul.hSMul, Units.mk0 and 10 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbit_superset_of_translations line 1016 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, Set, Membership.mem, Dickson.translationPGL, Dickson.ProjectiveLine, Dickson.orbitInfty, Dickson.P1point, LE.le, Union.union and 4 more
Proof uses: Set.union_subset, Iff.mpr, Set.singleton_subset_iff, Dickson.infty_mem_orbitInfty, Eq.mpr, Set.preimage, id, Eq, congrArg, propext, Set.image_subset_iff, And, Dickson.orbit_closed_under_translation
46 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Dickson.finite_subgroup_eq_roots_of_unity line 1030 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Finset, Dickson.K, GE.ge, OfNat.ofNat, Eq, Finset.card, Membership.mem, ZMod, HMul.hMul, Inv.inv, Ne, HPow.hPow
Proof uses: Not, rfl, Finset.image, Finset.eq_of_subset_of_card_le, Iff.mpr, LE.le, Finset.image_subset_iff, Eq.le, Eq.symm, Finset.card_image_of_injective, mul_left_cancel₀, Eq.rec, mul_right_cancel₀, Finset.prod, Finset.prod_ne_zero_iff, Trans.trans, Eq.mpr, id, congrArg, Finset.prod_const and 16 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilation_conjugation_formula line 1062 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, Exists, And, Ne, OfNat.ofNat, HMul.hMul, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Dickson.translationPGL and 1 more
Proof uses: Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Iff.mp, Dickson.fixesInfinity_iff_upperTriangular, Exists.intro, HDiv.hDiv, And.intro, div_ne_zero, left_ne_zero_of_mul, right_ne_zero_of_mul, Eq.rec, HasQuotient.Quotient, Subgroup, Dickson.upper_triangular_normalizes_translations, Eq.symm
72 instances, coercions and auxiliary constants left out.
theorem Dickson.dilation_param_mul line 1070 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, HMul.hMul, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.translationPGL, Inv.inv
Proof uses: Eq.mpr, id, congrArg, mul_inv_rev, Eq.symm, mul_assoc, Eq.refl
60 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilation_param_inv line 1077 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Ne, OfNat.ofNat, Eq, HMul.hMul, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Dickson.translationPGL, Inv.inv
Proof uses: Eq.mpr, id, congrArg, Eq.symm, mul_assoc, mul_inv_cancel₀, one_mul, Eq.refl, inv_inv, inv_mul_cancel, mul_one
83 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translationPGL_injective line 1087 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Function.Injective, Dickson.K, Dickson.PGLOf, ZMod, Dickson.translationPGL
Proof uses: Eq, Matrix, Fin, OfNat.ofNat, HMul.hMul, Matrix.GeneralLinearGroup, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Eq.mpr, Ne, Matrix.det, Not, id, congrFun', congrArg, Eq.trans, HSub.hSub and 69 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilation_param_one_is_translation line 1100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, HMul.hMul, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.translationPGL, Inv.inv, Exists
Proof uses: Ne, Matrix.GeneralLinearGroup.mkOfDetNeZero, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Iff.mp, Dickson.fixesInfinity_iff_upperTriangular, HDiv.hDiv, HasQuotient.Quotient, Subgroup, Dickson.upper_triangular_normalizes_translations, Eq.mp, congrArg, mul_one, Eq.symm, eq_of_div_eq_one, Dickson.translationPGL_injective, Exists.intro, right_ne_zero_of_mul and 90 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
theorem Dickson.same_dilation_param_diff_translation line 1131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, HMul.hMul, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.translationPGL, Inv.inv, Exists
Proof uses: Dickson.dilation_param_one_is_translation, Eq.mpr, id, congrArg, SemigroupAction.mul_smul, Iff.mpr, inv_smul_eq_iff, Eq.symm, Eq.refl, dite, mul_one, inv_mul_cancel, mul_assoc, Eq.mp, Dickson.translationPGL_zero, MulZeroClass.zero_mul, one_mul, mul_inv_cancel, Not, Dickson.dilation_param_mul and 3 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
def Dickson.dilationParam For g fixing ∞, the nonzero scalar c such that conjugation by g sends the translation by x to the translation by c x line 1155 source
Source documentation
For g fixing ∞, the nonzero scalar c such that conjugation by g sends the translation by x to the translation by c x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity
Proof uses: Exists.choose, And, Ne, OfNat.ofNat, HMul.hMul, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Dickson.translationPGL, Inv.inv, Dickson.dilation_conjugation_formula
34 instances, coercions and auxiliary constants left out.
```
noncomputable def dilationParam (g : PGLOf (K p)) (hg : g • infinity p = infinity p) : K p :=
…
```
Mentions: Dickson.PGLOf, Dickson.K, Dickson.infinity
theorem Dickson.dilationParam_ne_zero line 1159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, Ne, Dickson.dilationParam, OfNat.ofNat
Proof uses: And.left, Exists.choose, And, HMul.hMul, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Dickson.translationPGL, Inv.inv, Dickson.dilation_conjugation_formula, Exists.choose_spec
40 instances, coercions and auxiliary constants left out.
theorem Dickson.dilationParam_action line 1164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, HMul.hMul, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.translationPGL, Inv.inv, Dickson.dilationParam
Proof uses: And.right, Ne, Exists.choose, And, Dickson.dilation_conjugation_formula, Exists.choose_spec
57 instances, coercions and auxiliary constants left out.
theorem Dickson.dilationParam_mul_eq line 1169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, HMul.hMul, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, Dickson.dilationParam
Proof uses: Dickson.translationPGL, Inv.inv, Dickson.dilation_param_mul, Dickson.dilationParam_action, Eq.trans, Eq.symm, mul_one, Dickson.translationPGL_injective, Eq.mp, congrArg
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilationParam_one line 1178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.PGLOf, Dickson.K, ZMod, OfNat.ofNat, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Dickson.infinity, Dickson.dilationParam
Proof uses: HMul.hMul, Dickson.translationPGL, Inv.inv, Dickson.dilationParam_action, Eq.trans, Eq.symm, mul_one, Dickson.translationPGL_injective, Eq.mp, congrArg, one_mul, inv_one
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilationParam_eq_one_iff line 1185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Eq, Dickson.ProjectiveLine, HSMul.hSMul, Dickson.infinity, Iff, Dickson.dilationParam, OfNat.ofNat, Exists, Dickson.translationPGL
Proof uses: Iff.intro, Dickson.dilation_param_one_is_translation, HMul.hMul, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Inv.inv, Dickson.dilationParam_action, Eq.mp, congrArg, Eq.mpr, id, Neg.neg, Dickson.translationPGL_inv, HAdd.hAdd, Dickson.translationPGL_mul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr and 34 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Dickson.normalizer_element_fixes_infinity line 1197 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.map and 6 more
Proof uses: Dickson.sylowFixedPoint, Dickson.eq_sylow_fixedPoint, Subgroup.mem_map_of_mem, Eq.mpr, id, congrArg, Dickson.normalizer_stabilizes_fixedPoint, Dickson.sylow_element_fixes
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilationParam_scales_translationSet line 1213 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.map and 11 more
Proof uses: And, MonoidHom, Dickson.translationPGL, Inv.inv, Exists.intro, And.intro, Iff.mp, id, Eq.mpr, congrArg, Eq.refl, Dickson.dilationParam_action, Eq.mp
72 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Dickson.normDilationParam The dilation parameter of an element g of the normalizer of the Sylow p-subgroup P, as a scalar in K p line 1234 source
Source documentation
The dilation parameter of an element g of the normalizer of the Sylow p-subgroup P, as a scalar in K 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, Subgroup.map and 6 more
Proof uses: Dickson.dilationParam
46 instances, coercions and auxiliary constants left out.
```
noncomputable def normDilationParam
    (G : Subgroup (PGLOf (K p))) [Finite G]
    (hG_p : p ∣ Nat.card G)
    (P : Sylow p G)
    (hP_fix : ∀ g ∈ (P : Subgroup G).map (Subgroup.subtype G),
      g • infinity p = infinity p)
    (g : (Subgroup.normalizer ((P : Subgroup G) : Set G))) : K p :=
…
```
Mentions: Dickson.PGLOf, Dickson.K, Dickson.infinity
theorem Dickson.normDilationParam_of_P line 1244 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.map and 7 more
Proof uses: Iff.mpr, Dickson.dilationParam, Dickson.normalizer_element_fixes_infinity, Subtype.prop, Exists, Dickson.translationPGL, Dickson.dilationParam_eq_one_iff, Nontrivial, Iff.mp, LT.lt, Finite.one_lt_card_iff_nontrivial, HPow.hPow, Finsupp, Nat.factorization, Eq.mpr, Eq.refl, Sylow.card_eq_multiplicity, Eq.rec, one_lt_pow₀, Nat.Prime.one_lt and 30 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Dickson.same_normDilationParam_imp_coset line 1265 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.map and 9 more
Proof uses: Exists, Dickson.translationPGL, Exists.imp, mul_inv_eq_of_eq_mul, Dickson.same_dilation_param_diff_translation, Dickson.normalizer_element_fixes_infinity, Subtype.prop, Dickson.dilationParam_action, Eq.mpr, id, congrArg, HPow.hPow, Nat.recAux, pow_zero, zero_smul, Eq.symm, Dickson.translationPGL_zero, HAdd.hAdd, pow_succ', Dickson.translationPGL_mul and 18 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Dickson.normDilationParam_P_mul line 1294 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.map and 12 more
Proof uses: Dickson.normDilationParam_of_P, Eq.mpr, Dickson.dilationParam, id, congrArg, Dickson.normDilationParam.eq_1, Dickson.normalizer_element_fixes_infinity, Dickson.dilationParam_mul_eq, Eq.mp, one_mul, Eq.refl
68 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Dickson.normDilationParam_mul line 1315 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.map and 8 more
Proof uses: Dickson.dilationParam_mul_eq, Submonoid, Subgroup.toSubmonoid
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Dickson.normDilationParam_image_card line 1328 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 13 more
Proof uses: Set, Eq.mpr, id, congrArg, rfl, Set.ofPred, Exists, Trans.trans, Set.univ, Set.image, Subtype.mk, Subgroup.mul_mem, Subgroup.le_normalizer, Subtype.prop, Eq.rec, Eq.refl, Set.ext, Iff, Eq.trans, And and 62 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dilation_params_cover line 1397 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 17 more
Proof uses: Dvd.dvd, Eq.mpr, id, congrArg, dvd_mul_of_dvd_left, dvd_pow_self, Set.Finite, Set.range, Dickson.normDilationParam, Set.toFinite, Set.Finite.toFinset, Exists.intro, And.intro, Set.Finite.coe_toFinset, Set.ncard, Eq.symm, Set.ncard_coe_finset, Dickson.normDilationParam_image_card, propext, Set.Finite.mem_toFinset and 13 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
theorem Dickson.translationSet_card_eq_P line 1457 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.map and 7 more
Proof uses: Eq.mpr, id, congrArg, rfl, MulEquiv, Subgroup.equivMapOfInjective, Subgroup.subtype_injective, Nat.card_congr, MulEquiv.toEquiv, MulEquiv.symm, dite, Subsingleton, And.left, Nonempty, Iff.mp, And, Nat.card_eq_one_iff_unique, Eq.trans, Set, Singleton.singleton and 27 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbitInfty_ncard line 1480 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.map and 9 more
Proof uses: MulAction.stabilizer, Subgroup.normalizer, Subgroup.ext, Iff.intro, Dickson.fixes_infinity_normalizes_sylow, Dickson.normalizer_element_fixes_infinity, Set, MulAction.orbit, Set.ext, Exists.intro, Subtype.mk, And, And.intro, Subtype.prop, Eq.mpr, id, congrArg, Eq.symm, Nat.card_coe_set_eq, HasQuotient.Quotient and 5 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbit_eq_infty_union_translations line 1495 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 17 more
Proof uses: Eq.mpr, id, congrArg, rfl, Function.Injective, Units, Matrix.vecCons, Matrix.vecEmpty, Exists, Eq.mp, Projectivization.mk, Dickson.P1point.eq_1, congr_fun, Eq.symm, one_mul, mul_one, add_left_cancel, Disjoint, And, Not and 43 more
170 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbit_translate_conj line 1556 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, Set, Eq, Dickson.ProjectiveLine, Dickson.orbitInfty, Union.union, Singleton.singleton, Dickson.infinity, Set.image and 9 more
Proof uses: Eq.mpr, HSMul.hSMul, id, congrArg, Dickson.orbitInfty_conj_of_fixes_infty, Dickson.translation_smul_infinity, Set.image_union, Set.image_singleton, Union, Eq.rec, Eq.refl, Set.image_image, Set.image_congr, Membership.mem, Eq.trans, Dickson.translation_smul_P1point, add_comm, add_assoc, add_neg_cancel, add_zero
89 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbit_dilation_conj line 1574 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, Ne, Set, Eq, Dickson.ProjectiveLine, Dickson.orbitInfty, Union.union, Singleton.singleton, Dickson.infinity and 9 more
Proof uses: Eq.mpr, HSMul.hSMul, id, congrArg, Dickson.orbitInfty_conj_of_fixes_infty, Dickson.dilation_smul_infinity, Set.image_union, Set.image_singleton, Set.image_image, Union, Eq.rec, Eq.refl, Set.image_congr, Membership.mem, Dickson.dilation_smul_P1point
61 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbit_infty_eq_P1Fq_core line 1587 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 18 more
Proof uses: Dickson.P1point, Decidable.byContradiction, Not, Singleton.singleton, Iff.mpr, Set.eq_singleton_iff_unique_mem, And.intro, Dickson.infty_mem_orbitInfty, Or, Dickson.projLine_cases, absurd, Exists.intro, Eq.rec, Eq.symm, Set.ncard, Set.ncard_singleton, Fintype.card, Dickson.instFintypeSylow, Eq.trans, Dickson.orbitInfty_ncard and 62 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
def Dickson.conjEquiv The multiplicative isomorphism between G and its image k₀ G k₀⁻¹ under conjugation by k₀ line 1651 source
Source documentation
The multiplicative isomorphism between G and its image k₀ G k₀⁻¹ under conjugation by k₀.

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, MulEquiv, Subtype, Membership.mem, Subgroup.map, MulEquiv.toMonoidHom, MonoidHom, MulAut, MulAut.conj
Proof uses: Subgroup.equivMapOfInjective
46 instances, coercions and auxiliary constants left out.
```
def conjEquiv (G : Subgroup (PGLOf (K p))) (k₀ : PGLOf (K p)) :
    G ≃* (G.map (MulEquiv.toMonoidHom (MulAut.conj k₀))) :=
…
```
Mentions: Dickson.PGLOf, Dickson.K
def Dickson.sylowMap The image of the Sylow p-subgroup P under conjugation by k₀, as a Sylow p-subgroup of the conjugate group k₀ G k₀⁻¹ line 1658 source
Source documentation
The image of the Sylow p-subgroup P under conjugation by k₀, as a Sylow p-subgroup of the conjugate group k₀ G k₀⁻¹.

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, Subgroup.map, MulEquiv.toMonoidHom, MonoidHom, MulAut and 1 more
Proof uses: MulEquiv, Dickson.conjEquiv, Sylow.mk, IsPGroup, LE.le
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def sylowMap (G : Subgroup (PGLOf (K p))) [Finite G] (P : Sylow p G) (k₀ : PGLOf (K p)) :
    Sylow p (G.map (MulEquiv.toMonoidHom (MulAut.conj k₀))) :=
…
```
Mentions: Dickson.PGLOf, Dickson.K
theorem Dickson.exists_conj_sylow_fixing_infty line 1668 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, Exists, Sylow and 10 more
Proof uses: Classical.arbitrary, LE.le, Subgroup.map_subtype_le, Finite.of_injective, Subgroup.inclusion, Subgroup.inclusion_injective, Dickson.isPGroup_exists_common_fixedPoint, IsPGroup.map, Sylow.isPGroup', Dickson.exists_smul_eq_infinity, Exists.intro, Dickson.sylowMap, And, Iff.mp, Subgroup.mem_map, Subtype.mk, Dickson.conjEquiv, HMul.hMul, Inv.inv, Eq.symm and 8 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Dickson.orbit_infty_eq_P1Fq line 1692 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 12 more
Proof uses: Dvd.dvd, Eq.rec, dvd_mul_of_dvd_left, dvd_pow_self, ne_of_gt, Eq.symm, Sylow, Subgroup.subtype, HSMul.hSMul, Dickson.infinity, Dickson.exists_conj_sylow_fixing_infty, Finite.of_equiv, MulEquiv.toEquiv, Dickson.conjEquiv, Nat.card_congr, Eq.trans, And, Dickson.orbit_infty_eq_P1Fq_core, Eq.mpr, MonoidHom.comp and 13 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Dickson.pgl_conjugate_to_standard line 1724 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 12 more
Proof uses: Set, Dickson.ProjectiveLine, Dickson.orbitInfty, Dickson.P1Fq, Dickson.orbit_infty_eq_P1Fq, Exists.intro, LE.le, Dickson.preserves_P1Fq_in_range, Eq.rec, HSMul.hSMul, Dickson.preserves_orbitInfty, Eq.symm, Nat.card_congr, MulEquiv.toEquiv, Dickson.conjEquiv, Eq.trans, Set.range, Equiv.ofInjective, Dickson.pglMap_injective, RingHom.injective and 27 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Dickson.pgl_subgroups_conjugate line 1747 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 8 more
Proof uses: MonoidHom.range, GaloisField, Dickson.pglMap, Dickson.galoisFieldRingHom, Dickson.pgl_conjugate_to_standard, Exists.intro, Inv.inv, MonoidHom.comp, MulEquiv.symm, QuotientGroup.monoidHom_ext, MonoidHom.ext, HasQuotient.Quotient, QuotientGroup.mk', id, of_eq_true, Eq.trans, Int, Neg.neg, True, congr and 17 more
97 instances, coercions and auxiliary constants left out.

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

FLT/Slop/PGL2/FiniteSubgroups/FieldReconstruction.lean

Reconstructing a finite field from a wild subgroup of PGL₂(𝔽̄_p)

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

Reconstructing a finite field from a wild subgroup of `PGL₂(𝔽̄_p)`