linearCombination_comp_addSingleEquiv

English

Composing a linear combination with an addSingleEquiv yields a new linear combination with the last coordinate modified by the fixed vector i and coefficients c.

Русский

Составление линейной комбинации с addSingleEquiv даёт новую линейную комбинацию, где последняя координата изменена фиксированным вектором i и коэффициентами c.

LaTeX

$$$\big(\operatorname{linearCombination}_R\ v\big) \circ (\operatorname{addSingleEquiv}_i^c) = \operatorname{linearCombination}_R\ (v + (c \cdot\nobreak\cdot v_i))$$$

Lean4

theorem linearCombination_comp_addSingleEquiv (v : ι → M) :
    linearCombination R v ∘ₗ addSingleEquiv i c h₀ = linearCombination R (v + (c · • v i)) := by ext;
  simp [addSingleEquiv]

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