not_solvable — Mathlib

English

If a type X has at least five elements, then the permutation group on X is not solvable.

Русский

Если множество X содержит не менее пяти элементов, то группа перестановок на X неразрешима.

LaTeX

$$$5 \le |X| \Rightarrow \neg IsSolvable(Equiv.Perm X)$$$

Lean4

theorem not_solvable (X : Type*) (hX : 5 ≤ Cardinal.mk X) : ¬IsSolvable (Equiv.Perm X) :=
  by
  intro h
  have key : Nonempty (Fin 5 ↪ X) := by
    rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
  exact
    Equiv.Perm.fin_5_not_solvable
      (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))

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