linearCombination_comp — Mathlib

English

For f: α' → α, the linear combination over α' with v∘f equals the composition of the linearCombination over α with the domain-mapping lmapDomain.

Русский

Для отображения f: α' → α линейная комбинация над α с v∘f равна композиции линейной комбинации над α с отображением lmapDomain.

LaTeX

$$$\\operatorname{linearCombination}_R (v \\circ f) = (\\operatorname{linearCombination}_R v) \\circ (\\mathrm{lmapDomain}\\, R\\, R\\, f)$$$

Lean4

theorem linearCombination_comp (f : α' → α) :
    linearCombination R (v ∘ f) = (linearCombination R v).comp (lmapDomain R R f) :=
  by
  ext
  simp [linearCombination_apply]

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