lieAlgebra_isSolvable — Mathlib

English

If L' is solvable and f: L' → L is surjective, then L is solvable.

Русский

Если L' разрешимо и f сюръективен, то L разрешимо.

LaTeX

$$$\text{IsSolvable } L' \Rightarrow \text{IsSolvable } L$ under surjective f$$

Lean4

theorem lieAlgebra_isSolvable [hL' : IsSolvable L'] (h : Surjective f) : IsSolvable L :=
  by
  rw [isSolvable_iff R] at hL' ⊢
  apply hL'.imp
  intro k hk
  rw [← LieIdeal.derivedSeries_map_eq k h, hk]
  simp only [LieIdeal.map_eq_bot_iff, bot_le]

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