exists_eq_ad — Mathlib

English

Every derivation of a finite-dimensional Killing Lie algebra is inner; i.e., for every D there exists x with ad x = D.

Русский

Каждый вывод в конечномерной Killing-алгебре является внутренним: для каждого D существует x such that ad x = D.

LaTeX

$$∃ x, ad_{R,L}(x) = D.$$

Lean4

/-- Every derivation of a finite-dimensional Killing Lie algebra is an inner derivation. -/
theorem exists_eq_ad (D : 𝔻) : ∃ x, ad R L x = D := by
  change D ∈ 𝕀
  rw [range_ad_eq_top R L]
  exact Submodule.mem_top

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