commutator_lt_of_ne_bot — Mathlib

English

If a group is abelian, then it is solvable (a rephrasing of abelian implies solvable).

Русский

Если группа абелева, то она разрешима (продолжение): абелева ⇒ разрешима.

LaTeX

$$IsSolvable G$$

Lean4

theorem commutator_lt_of_ne_bot [IsSolvable G] {H : Subgroup G} (hH : H ≠ ⊥) : ⁅H, H⁆ < H :=
  by
  rw [← nontrivial_iff_ne_bot] at hH
  rw [← H.range_subtype, MonoidHom.range_eq_map, ← map_commutator, map_subtype_lt_map_subtype]
  exact commutator_lt_top_of_nontrivial H

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