linearCombination_comp_lmapDomain

English

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

Русский

Для линейного отображения $f$ выполняется; линейная комбинация через $v'$ равна композиции $f$ с линейной комбинацией через $v$.

LaTeX

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

Lean4

theorem linearCombination_comp_lmapDomain (f : α → α') :
    (linearCombination R v').comp (Finsupp.lmapDomain R R f) = linearCombination R (v' ∘ f) :=
  by
  ext
  simp

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