linearCombination_equivMapDomain — Mathlib

English

For any equivalence f: α ≃ α' we have (linearCombination_R v')(equivMapDomain f l) = linearCombination_R(v' ∘ f) l.

Русский

Для эквиваленции $f$ между индексами: линейная комбинация через $v'$ на $equivMapDomain f l$ равна линейной комбинации через $v'\circ f$ на $l$.

LaTeX

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

Lean4

@[simp]
theorem linearCombination_equivMapDomain (f : α ≃ α') (l : α →₀ R) :
    (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ f)) l := by
  rw [equivMapDomain_eq_mapDomain, linearCombination_mapDomain]

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