FinitePGroupMaximal.lean

theorem isCoatom_normal_of_isPGroup
    {p : ℕ} {G : Type u} [Group G] [Finite G] [Fact (Nat.Prime p)]
    (hG : IsPGroup p G) {M : Subgroup G} (hM : IsCoatom M) :
    M.Normal

theorem quotient_subgroup_eq_bot_or_eq_top_of_isCoatom
    {G : Type u} [Group G] {M : Subgroup G} [M.Normal]
    (hM : IsCoatom M) (K : Subgroup (G ⧸ M)) :
    K = ⊥ ∨ K = ⊤

theorem quotient_nontrivial_of_isCoatom
    {G : Type u} [Group G] {M : Subgroup G} [M.Normal]
    (hM : IsCoatom M) :
    Nontrivial (G ⧸ M)

theorem quotient_isCyclic_of_isCoatom
    {G : Type u} [Group G] {M : Subgroup G} [M.Normal]
    (hM : IsCoatom M) :
    IsCyclic (G ⧸ M)

theorem quotient_isSimpleGroup_of_isCoatom
    {G : Type u} [Group G] {M : Subgroup G} [M.Normal]
    (hM : IsCoatom M) :
    IsSimpleGroup (G ⧸ M)

theorem card_quotient_eq_prime_of_isCoatom_isPGroup
    {p : ℕ} {G : Type u} [Group G] [Finite G] [hp : Fact (Nat.Prime p)]
    (hG : IsPGroup p G) {M : Subgroup G} (hM : IsCoatom M) :
    Nat.card (G ⧸ M) = p