comp_L — Mathlib

English

Scalar multiplication commutes with lifting to derivations: (k • X).toDerivation = k • X.toDerivation.

Русский

Умножение на скаляр и преобразование к выводам коммутируют.

LaTeX

$$$ (k \cdot X)^{\mathrm{der}} = k \cdot X^{\mathrm{der}}. $$$

Lean4

theorem comp_L : (X f).comp (𝑳 I g) = X (f.comp (𝑳 I g)) :=
  by
  ext h
  rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply, fdifferential_apply,
    evalAt_apply]

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