isSimpleGroup_iff — Mathlib

English

A subgroup is simple if and only if it has no nontrivial normal subgroups and satisfies a standard subnormal condition.

Русский

Подгруппа простая тогда и только тогда, когда у неё нет ненулевых нормальных подгрупп и выполняется стандартное условие простоты.

LaTeX

$$IsSimpleGroup ↔ (nontrivial ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H)$$

Lean4

@[to_additive]
protected theorem isSimpleGroup_iff {H : Subgroup G} :
    IsSimpleGroup ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H :=
  by
  rw [isSimpleGroup_iff, H.nontrivial_iff_ne_bot, Subgroup.forall]
  simp +contextual [disjoint_of_le_iff_left_eq_bot, LE.le.ge_iff_eq]

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