coe_smul_linearMap — Mathlib

English

The equality of the action on the derivation and the action on its underlying linear map holds in the linear-map sense: ↑(r • D) = r • (D : A →ᴸ_R M).

Русский

Согласованность действия скаляра на деривацию и на связанное с ней линейное отображение: ↑(r • D) = r • (D : A →ᴸ_R M).

LaTeX

$$$\uparrow\bigl(r \cdot D\bigr) = r \cdot \bigl(D : A \to M\bigr)_{\text{as a linear map}},$$$

Lean4

@[simp]
theorem coe_smul_linearMap (r : S) (D : Derivation R A M) : ↑(r • D) = r • (D : A →ₗ[R] M) :=
  rfl

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