commutator_lt_top_of_nontrivial — Mathlib

English

If G is solvable and G is nontrivial, then the commutator subgroup is strictly smaller than the whole group.

Русский

Если G разрешима и не тривиальна, тоcommutator-подгруппа строго меньше всей группы.

LaTeX

$$[[H,H]] < H$$

Lean4

theorem commutator_lt_top_of_nontrivial [hG : IsSolvable G] [Nontrivial G] : commutator G < ⊤ :=
  by
  rw [lt_top_iff_ne_top]
  obtain ⟨n, hn⟩ := hG
  contrapose! hn
  refine ne_of_eq_of_ne ?_ top_ne_bot
  induction n with
  | zero => exact derivedSeries_zero G
  | succ n h => rwa [derivedSeries_succ, h]

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