derivedSeries_lt_top_of_solvable — Mathlib

English

If L is solvable and nontrivial, then its first derived series is strictly contained in the top subalgebra.

Русский

Если L разрешима и ненулево, то первая производящая серия строго содержится в сверху лежащей подалгебре.

LaTeX

$$$[IsSolvable\ L] \land [Nontrivial\ L] \Rightarrow \mathrm{derivedSeries}_{R} L 1 < \top$$$

Lean4

theorem derivedSeries_lt_top_of_solvable [IsSolvable L] [Nontrivial L] : derivedSeries R L 1 < ⊤ :=
  by
  obtain ⟨n, hn⟩ := IsSolvable.solvable (R := R) (L := L)
  rw [lt_top_iff_ne_top]
  intro contra
  rw [LieIdeal.derivedSeries_eq_top n contra] at hn
  exact top_ne_bot hn

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