coe_to_linearMap_comp — Mathlib

English

Composing a derivation with a linear map yields a new derivation; this operation is compatible with linear structure and scalar actions.

Русский

Составление деривации с линейным отображением даёт новую деривацию; операция совместима с линейной структурой и скалярными действиями.

LaTeX

$$$f : M \to_A N$ and D : Derivation R A M yield Derivation R A N via f \circ D$$$

Lean4

@[simp]
theorem coe_to_linearMap_comp : (f.compDer D : A →ₗ[R] N) = (f : M →ₗ[R] N).comp (D : A →ₗ[R] M) :=
  rfl

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