linearCombination_embDomain — Mathlib

English

For an embedding f: α ↪ α' and l ∈ α →₀ R, (linearCombination_R v') (embDomain f l) = linearCombination_R(v' ∘ f) l.

Русский

Для вложения $f: α \hookrightarrow α'$ и $l$, линейная комбинация через $v'$ на образе $l$ равна линейной комбинации через $v'\circ f$ на $l$.

LaTeX

$$$(\operatorname{linearCombination}_R v')(\operatorname{embDomain} f\, l) = \operatorname{linearCombination}_R(v'\circ f)\, l$$$

Lean4

@[simp]
theorem linearCombination_embDomain (f : α ↪ α') (l : α →₀ R) :
    (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ f)) l := by
  simp [linearCombination_apply, Finsupp.sum, support_embDomain, embDomain_apply]

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