# Simple groups #

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

## Main definitions #

• IsSimpleGroup G, a class indicating that a group has exactly two normal subgroups.

## Tags #

subgroup, subgroups

class IsSimpleGroup (G : Type u_1) [] extends :

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

• exists_pair_ne : ∃ (x : G) (y : G), x y
• eq_bot_or_eq_top_of_normal : ∀ (H : ), H.NormalH = H =

Any normal subgroup is either ⊥ or ⊤

Instances
theorem IsSimpleGroup.eq_bot_or_eq_top_of_normal {G : Type u_1} [] [self : ] (H : ) :
H.NormalH = H =

Any normal subgroup is either ⊥ or ⊤

class IsSimpleAddGroup (A : Type u_2) [] extends :

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

• exists_pair_ne : ∃ (x : A) (y : A), x y
• eq_bot_or_eq_top_of_normal : ∀ (H : ), H.NormalH = H =

Any normal additive subgroup is either ⊥ or ⊤

Instances
theorem IsSimpleAddGroup.eq_bot_or_eq_top_of_normal {A : Type u_2} [] [self : ] (H : ) :
H.NormalH = H =

Any normal additive subgroup is either ⊥ or ⊤

theorem AddSubgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [] [] {H : } (Hn : H.Normal) :
H = H =
theorem Subgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [] [] {H : } (Hn : H.Normal) :
H = H =
Equations
• =
Equations
• =
theorem IsSimpleAddGroup.isSimpleAddGroup_of_surjective {G : Type u_1} [] {H : Type u_3} [] [] [] (f : G →+ H) (hf : ) :
theorem IsSimpleGroup.isSimpleGroup_of_surjective {G : Type u_1} [] {H : Type u_3} [] [] [] (f : G →* H) (hf : ) :