theorem IsPGroup.not_le_normalizer {F : Type u_1} [Field F] {p : ℕ} [Fact (Nat.Prime p)] [CharP F p] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (H K : Subgroup ↥G) (hK : IsPGroup p ↥K) (H_lt_K : H < K) : ¬H ≤ K.normalizer

theorem Sylow.not_normal_subgroup_of_G {F : Type u_1} [Field F] {p : ℕ} [Fact (Nat.Prime p)] [CharP F p] (G K : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G] (Q : Sylow p ↥G) (hK : K ∈ MaximalAbelianSubgroups G) (hQK : Subgroup.map G.subtype (↑Q).normalizer = Subgroup.map G.subtype ↑Q ⊔ K) : ¬(↑Q).Normal

def R (F : Type u_1) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] (k : ℕ+) : Set F

Equations

• R F p k = {x : F | x ^ p ^ ↑k - x = 0}

instance field_R {F : Type u_1} [Field F] {p : ℕ} [Fact (Nat.Prime p)] [CharP F p] {k : ℕ+} : Field ↑(R F p k)

Equations

• field_R = sorry

@[reducible, inline]

abbrev SL (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] : Type (max 0 u_1 u_2)

Equations

• SL = Matrix.SpecialLinearGroup

theorem card_SL_field {𝔽 : Type u_1} [Field 𝔽] [Fintype 𝔽] (n : ℕ) : Nat.card (SL (Fin n) 𝔽) = Nat.card (GL (Fin n) 𝔽) / (Fintype.card 𝔽 - 1)

instance five_prime : Fact (Nat.Prime 5)

theorem dickson_classification_theorem_class_I {G : Type u_2} {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Prime p) (hp' : p = 0 ∨ (Nat.card G).Coprime p) (G✝ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G✝] : IsCyclic ↥G✝ ∨ ∃ (n : ℕ) (φ : ↥G✝ ≃* DihedralGroup n), True ∨ ∃ (φ : ↥G✝ ≃* Matrix.SpecialLinearGroup (Fin 2) (GaloisField 3 1)), True ∨ ∃ (φ : ↥G✝ ≃* Matrix.SpecialLinearGroup (Fin 2) (GaloisField 5 1)), True ∨ ∃ (φ : ↥G✝ ≃* GL (Fin 2) (GaloisField 3 1)), True

theorem dickson_classification_theorem_class_II {G : Type u_2} {F : Type u_1} [Field F] {p : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hp : Prime p) (hp' : p ∣ Nat.card G) (G✝ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G✝] : ∃ (Q : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)), IsElementaryAbelian p Q ∧ Q.Normal ∧ ∃ (φ : ↥G✝ ≃* ↥Q), True ∨ (p = 2 ∧ ∃ (n : ℕ) (φ : ↥G✝ ≃* DihedralGroup n), Odd n) ∨ ∃ (φ : ↥G✝ ≃* Matrix.SpecialLinearGroup (Fin 2) (GaloisField 5 1)), True ∨ ∃ (k : ℕ+) (φ : ↥G✝ ≃* GaloisField p ↑k), True ∨ ∃ (k : ℕ+) (x : GaloisField p (2 * ↑k)), orderOf x ^ 2 = p ^ ↑k ∧ ∃ (φ : ↥G✝ ≃* Matrix.SpecialLinearGroup (Fin 2) (GaloisField p ↑k)), True