lieAlgebra_isSolvable — Mathlib

English

If f is injective and L is solvable, then L' is solvable as well whenever there is an embedding f: L' → L.

Русский

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

LaTeX

$$$\text{IsSolvable } L \land \text{Injective } f \Rightarrow \text{IsSolvable } L'$$$

Lean4

theorem lieAlgebra_isSolvable [hL : IsSolvable L] (h : Injective f) : IsSolvable L' :=
  by
  rw [isSolvable_iff R] at hL ⊢
  apply hL.imp
  intro k hk
  apply LieIdeal.bot_of_map_eq_bot h; rw [eq_bot_iff, ← hk]
  apply LieIdeal.derivedSeries_map_le

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