Documentation

Mathlib.GroupTheory.Subgroup.Simple

Simple groups #

This file defines IsSimpleGroup G, a class indicating that a group has exactly two normal subgroups.

Main definitions #

Tags #

subgroup, subgroups

class IsSimpleGroup (G : Type u_1) [inst : Group G] extends Nontrivial :

A Group is simple when it has exactly two normal Subgroups.

Instances
    class IsSimpleAddGroup (A : Type u_1) [inst : AddGroup A] extends Nontrivial :

    An AddGroup is simple when it has exactly two normal AddSubgroups.

    Instances
      theorem Subgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [inst : Group G] [inst : IsSimpleGroup G] {H : Subgroup G} (Hn : Subgroup.Normal H) :
      H = H =
      theorem IsSimpleAddGroup.isSimpleAddGroup_of_surjective {G : Type u_2} [inst : AddGroup G] {H : Type u_1} [inst : AddGroup H] [inst : IsSimpleAddGroup G] [inst : Nontrivial H] (f : G →+ H) (hf : Function.Surjective f) :
      theorem IsSimpleGroup.isSimpleGroup_of_surjective {G : Type u_2} [inst : Group G] {H : Type u_1} [inst : Group H] [inst : IsSimpleGroup G] [inst : Nontrivial H] (f : G →* H) (hf : Function.Surjective f) :