eq_bot_or_eq_top — Mathlib

English

If G is a simple group, then any normal subgroup H of G is either trivial or the whole group.

Русский

Если G простая группа, то любая нормальная подгруппа H равна тривиальной или всей группе.

LaTeX

$$[IsSimpleGroup G] ⇒ (H.Normal → H = ⊥ ∨ H = ⊤)$$

Lean4

@[to_additive]
theorem eq_bot_or_eq_top [IsSimpleGroup G] {H : Subgroup G} (Hn : H.Normal) : H = ⊥ ∨ H = ⊤ :=
  IsSimpleGroup.eq_bot_or_eq_top_of_normal H Hn

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