ad_eq_lmul_left_sub_lmul_right — Mathlib

English

The adjoint representation ad_R A on an associative algebra A equals the difference of left and right multiplication operators.

Русский

Репрезентация адъекта ad_R A равна разности умножения слева и справа.

LaTeX

$$$\mathrm{ad}_{R,A} = \mathrm{mulLeft}_R - \mathrm{mulRight}_R$$$

Lean4

theorem ad_eq_lmul_left_sub_lmul_right (A : Type v) [Ring A] [Algebra R A] :
    (ad R A : A → Module.End R A) = LinearMap.mulLeft R - LinearMap.mulRight R := by ext a b;
  simp [LieRing.of_associative_ring_bracket]

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