# 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 #

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

## Tags #

subgroup, subgroups

class IsSimpleGroup (G : Type u_1) [inst : ] extends :
• Any normal subgroup is either ⊥⊥ or ⊤⊤

eq_bot_or_eq_top_of_normal : ∀ (H : ), H = H =

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

Instances
class IsSimpleAddGroup (A : Type u_1) [inst : ] extends :
• Any normal additive subgroup is either ⊥⊥ or ⊤⊤

eq_bot_or_eq_top_of_normal : ∀ (H : ), H = H =

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

Instances
theorem AddSubgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [inst : ] [inst : ] {H : } (Hn : ) :
H = H =
theorem Subgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [inst : ] [inst : ] {H : } (Hn : ) :
H = H =
Equations
• (_ : ) = (_ : )
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
theorem IsSimpleAddGroup.isSimpleAddGroup_of_surjective {G : Type u_2} [inst : ] {H : Type u_1} [inst : ] [inst : ] [inst : ] (f : G →+ H) (hf : ) :
theorem IsSimpleGroup.isSimpleGroup_of_surjective {G : Type u_2} [inst : ] {H : Type u_1} [inst : ] [inst : ] [inst : ] (f : G →* H) (hf : ) :