lie_coe_lieDerivation_apply — Mathlib

English

The Lie bracket with a derivation D, viewed as a linear map, coincides with the Lie bracket in the LieDerivation module: [x, D] = [x, D.toLinearMap].

Русский

Скобка Ли над элементом x и деривацией D, когда D воспринимается как линейное отображение, совпадает с корректной скобкой в модуле LieDerivation.

LaTeX

$$⟪x, (D : L →ₗ[R] M)⟫ = ⟪x, D⟫$$

Lean4

@[simp]
theorem lie_coe_lieDerivation_apply (x : L) (D : LieDerivation R L M) : ⁅x, (D : L →ₗ[R] M)⁆ = ⁅x, D⁆ := by ext; simp

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