isNilpotent_range — Mathlib

English

If L is nilpotent, then for any Lie algebra hom f: L → L', the range of f is nilpotent.

Русский

Если L нильпотентна, то образ любой гомоморфизм Ли L → L' является нильпотентным.

LaTeX

$$$\text{IsNilpotent } L \Rightarrow \text{IsNilpotent } (f.range)$$$

Lean4

theorem isNilpotent_range [IsNilpotent L] (f : L →ₗ⁅R⁆ L') : IsNilpotent f.range :=
  f.surjective_rangeRestrict.lieAlgebra_isNilpotent

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