FLT/KnownIn1980s/PGL2/Proofs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Proofs for the public PGL2 classification statements

This file imports the moved PGL2 development through its Dickson-classification endpoint and proves copies of the public statements from FLT.KnownIn1980s.PGL2.Defs.

Imports (2)
Imported by 1 file
  1. theorem Dickson.classification_tame_proof line 24 source

    standard axioms: Classical.choice, Quot.sound, propext 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: Dickson.classification_tame_slop, Fintype.ofFinite

    31 instances, coercions and auxiliary constants left out.

  2. theorem Dickson.classification_wild_proof line 37 source

    standard axioms: Classical.choice, Quot.sound, propext 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: Dickson.classification_wild_slop

    64 instances, coercions and auxiliary constants left out.