lmapDomain_linearCombination — Mathlib

English

For any f: α → α' and g: M →ₗ[R] M' with h: ∀i, g(v(i)) = v'(f(i)), we have (linearCombination_R v').comp (lmapDomain R R f) = g.comp (linearCombination_R v).

Русский

Для любого отображения $f$ между индексами и линейного отображения $g$, удовлетворяющего $g(v(i)) = v'(f(i))$, выполняется равенство композиции линейной комбинации и отображений.

LaTeX

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

Lean4

theorem lmapDomain_linearCombination (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) :
    (linearCombination R v').comp (lmapDomain R R f) = g.comp (linearCombination R v) :=
  by
  ext l
  simp [linearCombination_apply, h]

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