linearCombination_linear_comp — Mathlib

English

For any linear map f: M → M', linearCombination_R(v') = f ∘ linearCombination_R(v) where v' = f ∘ v.

Русский

Для любого линейного отображения $f: M\to M'$ выполняется $\operatorname{linearCombination}_R(v') = f \circ \operatorname{linearCombination}_R(v)$, если $v' = f\circ v$.

LaTeX

$$$\operatorname{linearCombination}_R(f\circ v) = f \circ \operatorname{linearCombination}_R(v).$$$

Lean4

theorem linearCombination_linear_comp (f : M →ₗ[R] M') : linearCombination R (f ∘ v) = f ∘ₗ linearCombination R v :=
  by
  ext
  simp [linearCombination_apply]

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