comm_iff_isSolvable — Mathlib

English

Let G be a simple group. Then G is solvable if and only if G is abelian.

Русский

Пусть G — простая группа. Тогда G разрешима тогда и только тогда, когда она абелева.

LaTeX

$$$\forall G\ (\ Group\ G\land IsSimpleGroup G\Rightarrow (IsSolvable G\iff \ Abelian G))$$$

Lean4

theorem comm_iff_isSolvable : (∀ a b : G, a * b = b * a) ↔ IsSolvable G :=
  ⟨isSolvable_of_comm, fun ⟨⟨n, hn⟩⟩ => by
    cases n
    · intro a b
      refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm <;>
        · rw [← hn]
          exact mem_top _
    · rw [IsSimpleGroup.derivedSeries_succ] at hn
      intro a b
      rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
      exact subset_closure ⟨a, b, rfl⟩⟩

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