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

34 declarations, 0 contain sorry, 0 declared as axioms

Basics on `SL₂`, its centre, and the image of `PSL₂` in `PGL₂`

This file proves the general facts about SL₂(F) and PSL₂(F) over a field F needed for Dickson's classification of finite subgroups of PGL₂(𝔽̄_p):

SL2.closure_elementary_eq_top: SL₂(F) is generated by the elementary matrices E12 a and E21 b;
SL2ToPGL_ker_eq_center and SL2_center_card: the kernel of SL₂(F) → PGL₂(F) is the centre {±1}, of order 2 when char F ≠ 2;
SL2_card: |SL₂(F)| = (q² - 1) * q for F a finite field with q elements;
PSLImageInPGL_index: for F finite of odd characteristic, the image of PSL₂(F) in PGL₂(F) has index 2, and index_two_subgroup_iso_PSL: it is the unique subgroup of index two consisting of the classes of matrices with square determinant;
PSL2_ZMod3_equiv_GF31: the identification PSL₂(𝔽₃) ≃* A₄ obtained by letting SL₂(𝔽₃) act on the four points of ℙ¹(𝔽₃).

Imports (4)

Imported by 2 files

theorem mem_of_odd_orderOf_of_index_two line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, Nat, Subgroup.index, OfNat.ofNat, Odd, orderOf, Membership.mem
Proof uses: HAdd.hAdd, HMul.hMul, HPow.hPow, Eq.mpr, id, congrArg, Eq.symm, pow_mul, pow_succ, pow_orderOf_eq_one, Eq.refl, Inv.inv, eq_inv_of_mul_eq_one_right, Subgroup.inv_mem, Subgroup.pow_mem, Subgroup.sq_mem_of_index_two
41 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def SL2.E12 The elementary matrix e₁₂ a = !![1, a; 0, 1] as an element of SL₂(F) line 68 source
Source documentation
The elementary matrix e₁₂ a = !![1, a; 0, 1] as an element of SL₂(F).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Nat
Proof uses: Subtype.mk, Matrix, Eq, Matrix.det, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def SL2.E12 (a : F) : Matrix.SpecialLinearGroup (Fin 2) F :=
…
```
def SL2.E21 The elementary matrix e₂₁ b = !![1, 0; b, 1] as an element of SL₂(F) line 75 source
Source documentation
The elementary matrix e₂₁ b = !![1, 0; b, 1] as an element of SL₂(F).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Nat
Proof uses: Subtype.mk, Matrix, Eq, Matrix.det, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def SL2.E21 (b : F) : Matrix.SpecialLinearGroup (Fin 2) F :=
…
```
theorem SL2.closure_elementary_eq_top line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Eq, Subgroup, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Nat, Subgroup.closure, Union.union, Set, Set.range, SL2.E12, SL2.E21, Top.top
Proof uses: Iff.mpr, LE.le, eq_top_iff, Membership.mem, Subgroup.subset_closure, Or.inl, Exists.intro, rfl, Or.inr, Ne, Matrix, Matrix.det, HMul.hMul, HDiv.hDiv, HSub.hSub, Matrix.SpecialLinearGroup.ext, Unit, Eq.mpr, HAdd.hAdd, id and 89 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
def SL2ToPGL The natural homomorphism SL₂(F) → PGL₂(F) sending a matrix to the class of its image in GL₂(F) line 150 source
Source documentation
The natural homomorphism SL₂(F) → PGL₂(F) sending a matrix to the class of its image in GL₂(F).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, MonoidHom, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Nat, Dickson.PGLOf, Matrix.GeneralLinearGroup, Matrix, Subgroup.center
Proof uses: MonoidHom.comp, HasQuotient.Quotient, Subgroup, QuotientGroup.mk', Matrix.SpecialLinearGroup.toGL
35 instances, coercions and auxiliary constants left out.
```
def SL2ToPGL (F : Type*) [Field F] : Matrix.SpecialLinearGroup (Fin 2) F →* PGLOf F :=
…
```
def PSLImageInPGL The image of PSL₂(F) inside PGL₂(F), namely the range of SL2ToPGL F line 155 source
Source documentation
The image of PSL₂(F) inside PGL₂(F), namely the range of SL2ToPGL F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Subgroup, Dickson.PGLOf, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Matrix, Subgroup.center
Proof uses: MonoidHom.range, Matrix.SpecialLinearGroup, SL2ToPGL
24 instances, coercions and auxiliary constants left out.
```
def PSLImageInPGL (F : Type*) [Field F] : Subgroup (PGLOf F) :=
…
```
theorem PGL.orderOf_E12_image line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Field, CharP, Ne, OfNat.ofNat, Eq, orderOf, Dickson.PGLOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, MonoidHom, Matrix.SpecialLinearGroup, SL2ToPGL, SL2.E12
Proof uses: orderOf_eq_prime, HPow.hPow, HMul.hMul, Nat.recAux, Eq.mpr, id, congrArg, pow_zero, Matrix.SpecialLinearGroup.ext, Matrix.det, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Matrix.one_fin_two, Nat.cast_zero, MulZeroClass.zero_mul, Eq.refl, HAdd.hAdd, pow_succ and 72 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
theorem PSLImageInPGL_le_of_index_two line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Field, CharP, Fintype, Subgroup, Dickson.PGLOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Eq, Subgroup.index, LE.le, PSLImageInPGL
Proof uses: Fact.out, inferInstance, Ne, orderOf, MonoidHom, Matrix.SpecialLinearGroup, SL2ToPGL, SL2.E21, orderOf_eq_prime, HPow.hPow, HMul.hMul, Nat.recAux, Matrix.SpecialLinearGroup.ext, id, Matrix.det, Eq.mpr, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty and 95 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
theorem SL2ToPGL_ker_eq_center line 275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Eq, Subgroup, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Nat, MonoidHom.ker, Dickson.PGLOf, Matrix.GeneralLinearGroup, Matrix, Subgroup.center, SL2ToPGL
Proof uses: Subgroup.ext, Iff.intro, Membership.mem, id, MonoidHom, HasQuotient.Quotient, Matrix.SpecialLinearGroup.toGL, Eq.mpr, HMul.hMul, congrArg, propext, Subgroup.mem_center_iff, Subtype.ext, Matrix.det, congr_arg, Units, Eq.mp, QuotientGroup.eq_one_iff, MonoidHom.mem_ker, Equiv and 29 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
theorem SL2_center_card line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, GT.gt, OfNat.ofNat, Field, CharP, Eq, Nat.card, Subtype, Matrix.SpecialLinearGroup, Fin, Membership.mem, Subgroup, Subgroup.center
Proof uses: Fact.out, inferInstance, Subgroup.zpowers, Neg.neg, le_antisymm, Matrix, HMul.hMul, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Matrix.det, congr_arg, SL2.E12, Eq.mp, congrArg, propext, Subgroup.mem_center_iff, SL2.E21, congr_fun and 85 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
theorem SL2_card line 421 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Fintype, GE.ge, Nat, Fintype.card, OfNat.ofNat, Eq, Nat.card, Matrix.SpecialLinearGroup, Fin, HMul.hMul, HSub.hSub, HPow.hPow
Proof uses: Function.Surjective, Matrix.GeneralLinearGroup, Units, MonoidHom, Matrix, Matrix.GeneralLinearGroup.det, Exists.intro, Units.mk, Matrix.diagonal, Matrix.vecCons, Matrix.vecEmpty, Inv.inv, Eq.mpr, id, congrArg, Matrix.diagonal_mul_diagonal, Eq.symm, Matrix.diagonal_one, congr_arg, funext and 55 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
theorem PSLImageInPGL_index line 475 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, GT.gt, OfNat.ofNat, Field, CharP, Fintype, GE.ge, Fintype.card, Eq, Subgroup.index, Dickson.PGLOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, PSLImageInPGL
Proof uses: HMul.hMul, Nat.card, Subtype, Membership.mem, Subgroup, HSub.hSub, HPow.hPow, Matrix.SpecialLinearGroup, MonoidHom.ker, SL2ToPGL, Subgroup.card_mul_index, id, MonoidHom.range, Eq.trans, mul_comm, Eq.mp, congrArg, SL2_card, le_trans, Mathlib.Meta.NormNum.isNat_le_true and 92 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem index_two_subgroup_iso_PSL line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Field, CharP, Fintype, GE.ge, Fintype.card, Subgroup, Dickson.PGLOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Eq, Subgroup.index, Nonempty, MulEquiv and 4 more
Proof uses: LE.le, PSLImageInPGL, PSLImageInPGL_le_of_index_two, PSLImageInPGL_index, SetLike.ext', Set.eq_of_subset_of_card_le, Set, HMul.hMul, Eq.mpr, Nat.card, id, congrArg, Eq.symm, Nat.card_eq_fintype_card, Eq.trans, Subgroup.card_mul_index, Eq.le, Nat.eq_of_mul_eq_mul_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat and 28 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma PSL2_ZMod3_equiv_GF31 line 516 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nonempty, MulEquiv, Matrix.ProjectiveSpecialLinearGroup, Fin, OfNat.ofNat, Nat, ZMod, GaloisField, Matrix.SpecialLinearGroup, Subgroup.center
Proof uses: RingEquiv, AlgEquiv.toRingEquiv, AlgEquiv.symm, GaloisField.equivZmodP, MulEquiv.mk, Equiv.mk, MonoidHom, Matrix.SpecialLinearGroup.map, RingEquiv.toRingHom, RingEquiv.symm, Subtype.ext, Matrix, Eq, Matrix.det, Matrix.ext, RingEquiv.symm_apply_apply, RingEquiv.apply_symm_apply, MonoidHom.map_mul, Nonempty.intro, QuotientGroup.congr and 24 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
abbrev SL2F3 The special linear group SL₂(𝔽₃) line 541 source
Source documentation
The special linear group SL₂(𝔽₃).

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Nat, ZMod
4 instances, coercions and auxiliary constants left out.
```
abbrev SL2F3 := SpecialLinearGroup (Fin 2) (ZMod 3)
```
abbrev PSL2F3 The projective special linear group PSL₂(𝔽₃) line 543 source
Source documentation
The projective special linear group PSL₂(𝔽₃).

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Matrix.ProjectiveSpecialLinearGroup, Fin, OfNat.ofNat, Nat, ZMod
4 instances, coercions and auxiliary constants left out.
```
abbrev PSL2F3 := ProjectiveSpecialLinearGroup (Fin 2) (ZMod 3)
```
def p1Rep A choice of representative vector in 𝔽₃² for each of the four points of ℙ¹(𝔽₃) line 546 source
Source documentation
A choice of representative vector in 𝔽₃² for each of the four points of ℙ¹(𝔽₃).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod
Proof uses: p1Rep.match_1, Unit, Matrix.vecCons, Matrix.vecEmpty
19 instances, coercions and auxiliary constants left out.
```
def p1Rep : Fin 4 → Fin 2 → ZMod 3
  | 0 => ![1, 0] | 1 => ![0, 1] | 2 => ![1, 1] | 3 => ![1, 2]

/-- In `ZMod 3` every element is its own inverse, so we can use `v 0 * v 1` in place of
`v 0 * (v 1)⁻¹` (the latter does not reduce definitionally, since `ZMod.inv` is defined
via `Nat.gcdA`). -/
```
def p1Proj Documented declaration: p1Proj line 552 source
Source documentation
In ZMod 3 every element is its own inverse, so we can use v 0 * v 1 in place of v 0 * (v 1)⁻¹ (the latter does not reduce definitionally, since ZMod.inv is defined via Nat.gcdA).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod
Proof uses: ite, Eq, HMul.hMul
23 instances, coercions and auxiliary constants left out.
```
def p1Proj (v : Fin 2 → ZMod 3) : Fin 4 :=
…
```
def p1Act The action of a matrix M on the four points of ℙ¹(𝔽₃), obtained by applying M to a representative vector and projecting back line 559 source
Source documentation
The action of a matrix M on the four points of ℙ¹(𝔽₃), obtained by applying M to a representative vector and projecting back.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod
Proof uses: p1Proj, Matrix.mulVec, p1Rep
8 instances, coercions and auxiliary constants left out.
```
def p1Act (M : Matrix (Fin 2) (Fin 2) (ZMod 3)) : Fin 4 → Fin 4 :=
…
```
lemma p1Proj_smul line 562 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Fin, Eq, p1Proj, HSMul.hSMul
Proof uses: HMul.hMul, List, List.Mem, HAdd.hAdd, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, absurd, rfl, eq_of_heq, List.Mem.tail and 47 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma p1Rep_p1Proj_scalar line 575 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Not, And, Eq, Exists, Ne, Fin, p1Rep, p1Proj, Matrix.vecCons, Matrix.vecEmpty, HSMul.hSMul, Nat.succ
Proof uses: absurd, And.intro, rfl, Exists.intro, one_ne_zero, funext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil and 14 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma sl2_mulVec_ne_zero line 585 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SL2F3, Fin, OfNat.ofNat, Nat, ZMod, Ne, Matrix.mulVec, Matrix, Eq, Matrix.det
Proof uses: Matrix.mulVec_injective_of_isUnit, Eq.mpr, IsUnit, id, congrArg, propext, Matrix.isUnit_iff_isUnit_det, Subtype.prop, isUnit_one, Matrix.mulVec_zero, Eq.refl
52 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma p1Rep_ne_zero line 590 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, ZMod, p1Rep
Proof uses: Eq, False, absurd, congr_fun
27 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma p1Proj_mulVec_rep_proj line 598 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Ne, Eq, p1Proj, Matrix.mulVec, p1Rep
Proof uses: And, Matrix.vecCons, Matrix.vecEmpty, HSMul.hSMul, Nat.succ, Exists, p1Rep_p1Proj_scalar, False, funext, Unit, Eq.mpr, id, congrArg, rfl, Matrix.mulVec_smul, p1Proj_smul, Eq.refl
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance sl2F3MulAction line 604 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MulAction, SL2F3, Fin, OfNat.ofNat, Nat, ZMod
Proof uses: MulAction.mk, SemigroupAction.mk, SMul.mk, p1Act, Matrix, Eq, Matrix.det
19 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def sl2F3ToPermHom The permutation representation SL₂(𝔽₃) → S₄ induced by the action on ℙ¹(𝔽₃) line 613 source
Source documentation
The permutation representation SL₂(𝔽₃) → S₄ induced by the action on ℙ¹(𝔽₃).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MonoidHom, SL2F3, Equiv.Perm, Fin, OfNat.ofNat, Nat, ZMod
Proof uses: MulAction.toPermHom
16 instances, coercions and auxiliary constants left out.
```
def sl2F3ToPermHom : SL2F3 →* Equiv.Perm (Fin 4) := MulAction.toPermHom _ _
```
Mentions: SL2F3
def U₁ The upper elementary generator !![1, 1; 0, 1] of SL₂(𝔽₃) line 616 source
Source documentation
The upper elementary generator !![1, 1; 0, 1] of SL₂(𝔽₃).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SL2F3
Proof uses: Subtype.mk, Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.det, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def U₁ : SL2F3 := ⟨!![1, 1; 0, 1], by rw [det_fin_two]; rfl⟩
```
Mentions: SL2F3
def L₁ The lower elementary generator !![1, 0; 1, 1] of SL₂(𝔽₃) line 618 source
Source documentation
The lower elementary generator !![1, 0; 1, 1] of SL₂(𝔽₃).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SL2F3
Proof uses: Subtype.mk, Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.det, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def L₁ : SL2F3 := ⟨!![1, 0; 1, 1], by rw [det_fin_two]; rfl⟩
```
Mentions: SL2F3
lemma central_is_scalar line 620 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SL2F3, Eq, HMul.hMul, Fin, OfNat.ofNat, Nat, ZMod, U₁, L₁, And, Matrix, Matrix.det
Proof uses: congr_fun, congr_arg, Subtype, Eq.symm, add_left_cancel, Eq.mp, HAdd.hAdd, congr, congrArg, Eq.trans, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Finset.sum, Finset.univ, Fintype, Mul, AddCommMonoid, Matrix.mul_apply and 17 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma scalar_det_one_pm_one line 631 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SL2F3, Eq, ZMod, OfNat.ofNat, Nat, Matrix, Fin, Matrix.det, Or, Neg.neg
Proof uses: Subtype.prop, Iff.mp, HPow.hPow, sq_eq_one_iff, Eq.mp, HMul.hMul, congrArg, Eq.symm, sq, HSub.hSub, sub_zero, MulZeroClass.mul_zero, Matrix.det_fin_two, Or.inl, Matrix.SpecialLinearGroup.ext, Unit, Eq.trans, Or.inr
77 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma kernel_is_scalar line 652 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SL2F3, Eq, Fin, OfNat.ofNat, Nat, p1Act, Matrix, ZMod, Matrix.det, And
Proof uses: dite, Not, HMul.hMul, absurd, Eq.mp, ite, congrFun', congrArg, ite_eq_left, ite_eq_right, ite_congr, Matrix.mulVec, p1Rep, Eq.trans, Finset.sum, Finset.univ, Matrix.vecCons, Matrix.vecEmpty, HAdd.hAdd, Fin.sum_univ_two and 42 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
lemma sl2F3_ker_eq_center line 685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Subgroup, SL2F3, Fin, OfNat.ofNat, Nat, ZMod, MonoidHom.ker, Equiv.Perm, sl2F3ToPermHom, Subgroup.center
Proof uses: Subgroup.ext, Eq.mpr, Iff, Membership.mem, MonoidHom, id, congrArg, propext, MonoidHom.mem_ker, HMul.hMul, Subgroup.mem_center_iff, Iff.intro, p1Act, Matrix, Matrix.det, Iff.mp, Equiv, Equiv.ext_iff, And, kernel_is_scalar and 37 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
theorem A4_iso_PSL2_F3 line 701 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nonempty, MulEquiv, Subtype, Equiv.Perm, Fin, OfNat.ofNat, Nat, Membership.mem, Subgroup, alternatingGroup, Matrix.ProjectiveSpecialLinearGroup, ZMod, Matrix.SpecialLinearGroup, Subgroup.center
Proof uses: MonoidHom, SL2F3, MonoidHom.codRestrict, sl2F3ToPermHom, Eq.mpr, Eq, Units, Int, Equiv.Perm.sign, id, congrArg, propext, Equiv.Perm.mem_alternatingGroup, List, List.Mem, Matrix, Matrix.det, List.pmap, Subtype.mk, List.filter and 79 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
theorem A4_iso_PSL2_GF31 line 725 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nonempty, MulEquiv, Subtype, Equiv.Perm, Fin, OfNat.ofNat, Nat, Membership.mem, Subgroup, alternatingGroup, Matrix.ProjectiveSpecialLinearGroup, GaloisField, Matrix.SpecialLinearGroup, Subgroup.center
Proof uses: ZMod, A4_iso_PSL2_F3, PSL2_ZMod3_equiv_GF31, Nonempty.intro, MulEquiv.trans
38 instances, coercions and auxiliary constants left out.

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

FLT/Slop/PGL2/FiniteSubgroups/PSLBasic.lean

Basics on SL₂, its centre, and the image of PSL₂ in PGL₂

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

Basics on `SL₂`, its centre, and the image of `PSL₂` in `PGL₂`