linearCombination_mapDomain — Mathlib

English

For any f: α → α' we have (linearCombination_R v').comp (lmapDomain R R f) = linearCombination_R (v' ∘ f).

Русский

Для любого отображения $f$ между индексами выполняется: линейная комбинация через $v'$ после $lmapDomain$ равна линейной комбинации через $v'\circ f$.

LaTeX

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

Lean4

@[simp]
theorem linearCombination_mapDomain (f : α → α') (l : α →₀ R) :
    (linearCombination R v') (mapDomain f l) = (linearCombination R (v' ∘ f)) l :=
  LinearMap.congr_fun (linearCombination_comp_lmapDomain _ _) l

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