lie_der_ad_eq_ad_der — Mathlib

English

The commutator of a derivation with an ad-derivation equals the ad-derivation of the image: [D, ad x] = ad(Dx).

Русский

Свойство: [D, ad x] = ad(Dx).

LaTeX

$$$[D,\\, ad\\;R\\;L\\; x] = ad\\;R\\;L\\; (D x)$$$

Lean4

/-- The commutator of a derivation `D` and a derivation of the form `ad x` is `ad (D x)`. -/
theorem lie_der_ad_eq_ad_der (D : LieDerivation R L L) (x : L) : ⁅D, ad R L x⁆ = ad R L (D x) := by
  rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]

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