fromCols_mulVec — Mathlib

English

For A1, A2 and v, the product (fromCols A1 A2) *ᵥ v equals A1 *ᵥ (v ∘ Sum.inl) plus A2 *ᵥ (v ∘ Sum.inr).

Русский

Для A1, A2 и v произведение (fromCols A1 A2) *ᵥ v равно A1 *ᵥ (v ∘ Sum.inl) плюс A2 *ᵥ (v ∘ Sum.inr).

LaTeX

$$$$ (\operatorname{fromCols} A_1 A_2) *ᵥ v = A_1 *ᵥ (v \circ \mathrm{Sum.inl}) + A_2 *ᵥ (v \circ \mathrm{Sum.inr}). $$$$

Lean4

@[simp]
theorem fromCols_mulVec [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v : n₁ ⊕ n₂ → R) :
    fromCols A₁ A₂ *ᵥ v = A₁ *ᵥ v ∘ Sum.inl + A₂ *ᵥ v ∘ Sum.inr := by simp [← fromCols_mulVec_sumElim]

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