fromCols_mulVec_sumElim — Mathlib

English

For A1, A2 and v1, v2, the product fromCols(A1,A2) with Sum.elim v1 v2 equals A1*v1 plus A2*v2: fromCols A1 A2 *ᵥ Sum.elim v1 v2 = A1 *ᵥ v1 + A2 *ᵥ v2.

Русский

Пусть A1, A2 и v1, v2. Произведение fromCols(A1,A2) на Sum.elim v1 v2 равно A1*v1 плюс A2*v2: fromCols A1 A2 *ᵥ Sum.elim v1 v2 = A1 *ᵥ v1 + A2 *ᵥ v2.

LaTeX

$$$$ \operatorname{fromCols}(A_1,A_2) *ᵥ \Sum.elim v_1 v_2 = A_1 *ᵥ v_1 + A_2 *ᵥ v_2. $$$$

Lean4

theorem fromCols_mulVec_sumElim [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R)
    (v₂ : n₂ → R) : fromCols A₁ A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂ :=
  by
  ext
  simp [Matrix.mulVec, fromCols]

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