isSolvable_range — Mathlib

English

If L is solvable, then the range of any Lie homomorphism from a solvable source is solvable.

Русский

Если L разрешимо, то образ любого гомоморфизма Ли из разрешимого источника разрешим.

LaTeX

$$$\text{IsSolvable } L \Rightarrow \text{IsSolvable } \operatorname{range}(f)$$$

Lean4

instance isSolvable_range (f : L' →ₗ⁅R⁆ L) [LieAlgebra.IsSolvable L'] : LieAlgebra.IsSolvable f.range :=
  f.surjective_rangeRestrict.lieAlgebra_isSolvable

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