not_solvable_of_mem_derivedSeries

English

Let G be a group and g ∈ G with g ≠ 1, such that g ∈ derivedSeries(G,n) for every n. Then G is not solvable.

Русский

Пусть G — группа и есть элемент g ∈ G такой, что g ≠ 1 и ∀ n: g ∈ derivedSeries(G,n). Тогда G неразрешима.

LaTeX

$$$\forall G\ (Group\ G)\ \forall g\in G,\ g\neq 1\land (\forall n:\mathbb{N},\ g\in derivedSeries(G,n))\Rightarrow \neg IsSolvable(G)$$$

Lean4

theorem not_solvable_of_mem_derivedSeries {g : G} (h1 : g ≠ 1) (h2 : ∀ n : ℕ, g ∈ derivedSeries G n) : ¬IsSolvable G :=
  mt (isSolvable_def _).mp
    (not_exists_of_forall_not fun n h => h1 (Subgroup.mem_bot.mp ((congr_arg (g ∈ ·) h).mp (h2 n))))

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