instIsSimpleOrderSubgroup — Mathlib

English

If C is a commutative simple group, then the lattice of subgroups of C is simple; i.e., IsSimpleOrder (Subgroup C).

Русский

Если C — коммуникативная простая группа, то решетка подгрупп C проста; то есть IsSimpleOrder (Subgroup C).

LaTeX

$$IsSimpleOrder (Subgroup C)$$

Lean4

@[to_additive]
instance {C : Type*} [CommGroup C] [IsSimpleGroup C] : IsSimpleOrder (Subgroup C) :=
  ⟨fun H => H.normal_of_comm.eq_bot_or_eq_top⟩

Похожие утверждения