mathlib3 documentation

group_theory.subgroup.simple

Simple groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Tags #

subgroup, subgroups

@[instance]
@[class]
structure is_simple_group (G : Type u_1) [group G] :
Prop

A group is simple when it has exactly two normal subgroups.

Instances of this typeclass
@[class]
structure is_simple_add_group (A : Type u_2) [add_group A] :
Prop

An add_group is simple when it has exactly two normal add_subgroups.

theorem subgroup.normal.eq_bot_or_eq_top {G : Type u_1} [group G] [is_simple_group G] {H : subgroup G} (Hn : H.normal) :
H = H =