English
The permutation group on five elements is not solvable.
Русский
Группа перестановок над множеством из пяти элементов неразрешима.
LaTeX
$$$\neg IsSolvable\left(Equiv.Perm (Fin 5)\right)$$$
Lean4
theorem fin_5_not_solvable : ¬IsSolvable (Equiv.Perm (Fin 5)) :=
by
let x : Equiv.Perm (Fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], by decide, by decide⟩
let y : Equiv.Perm (Fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], by decide, by decide⟩
let z : Equiv.Perm (Fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], by decide, by decide⟩
have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide
refine not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_
induction n with
| zero => exact mem_top x
| succ n ih =>
rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)
