FLT/KnownIn1980s/PGL2/Defs.lean

GitHub source file

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

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

5 declarations, 2 contain sorry, 0 declared as axioms

Public statements for Dickson's classification in PGL₂

This file contains the non-slop API for the PGL2 classification statements. The proofs live in FLT.KnownIn1980s.PGL2.Proofs, which imports the AI-generated development in FLT.Slop.PGL2.

Imports (8)
Imported by 3 files
  1. abbrev Dickson.K An algebraic closure K p of the finite field 𝔽_p = ZMod p line 32 source

    Source documentation

    An algebraic closure K p of the finite field 𝔽_p = ZMod p.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime

    Proof uses: AlgebraicClosure, ZMod

    1 instances, coercions and auxiliary constants left out.

    noncomputable abbrev K : Type := AlgebraicClosure (ZMod p)
  2. abbrev Dickson.PGL The projective general linear group PGL₂(K p), i.e. GL₂(K p) modulo its centre line 35 source

    Source documentation

    The projective general linear group PGL₂(K p), i.e. GL₂(K p) modulo its centre.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime

    Proof uses: Matrix.ProjGenLinGroup, Fin, OfNat.ofNat, Dickson.K, ZMod

    5 instances, coercions and auxiliary constants left out.

    abbrev PGL : Type := Matrix.ProjGenLinGroup (Fin 2) (K p)

    Mentions: Dickson.K

  3. abbrev Dickson.PSL The projective special linear group PSL₂(K p) line 38 source

    Source documentation

    The projective special linear group PSL₂(K p).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fact, Nat.Prime

    Proof uses: Matrix.ProjectiveSpecialLinearGroup, Fin, OfNat.ofNat, Dickson.K, ZMod

    5 instances, coercions and auxiliary constants left out.

    abbrev PSL : Type := Matrix.ProjectiveSpecialLinearGroup (Fin 2) (K p)
…

    Mentions: Dickson.K

  4. theorem Dickson.classification_tame sorry line 42 source

    depends on sorry what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGL, Fin, Dickson.K, ZMod, Finite, Subtype, Membership.mem, Not, Dvd.dvd, Nat.card, Nontrivial, Or, IsCyclic, Exists and 7 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  5. theorem Dickson.classification_wild sorry line 52 source

    depends on sorry what this means

    Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGL, Fin, Dickson.K, ZMod, Finite, Subtype, Membership.mem, Dvd.dvd, Nat.card, Or, Exists, GE.ge, Nat.Coprime, HSub.hSub and 18 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    108 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.