mem_ad_idealRange_iff — Mathlib

English

A further characterization: a derivation D lies in the idealRange of ad iff D = ad x for some x.

Русский

Дополнительное характеристическое предложение: D = ad x для некоторого x.

LaTeX

$$$D\\in (ad\\,R\\,L).idealRange\\iff \\exists x:\\, L,\\; ad\\,R\\,L\\; x = D$$$

Lean4

/-- A derivation `D` belongs to the ideal range of the adjoint action iff it is of the form `ad x`
for some `x` in the Lie algebra `L`. -/
theorem mem_ad_idealRange_iff {D : LieDerivation R L L} : D ∈ (ad R L).idealRange ↔ ∃ x : L, ad R L x = D :=
  (ad R L).mem_idealRange_iff (ad_isIdealMorphism R L)

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