fromRows_mulVec — Mathlib

English

Two column-partitioned matrices are equal exactly when their left and right blocks are equal: fromCols A1 A2 = fromCols B1 B2 iff A1 = B1 ∧ A2 = B2.

Русский

Две матрицы, разбиенные по столбцам, равны тогда и только тогда, когда их левый и правый блоки равны: fromCols A1 A2 = fromCols B1 B2 ⇔ A1 = B1 ∧ A2 = B2.

LaTeX

$$$$ \operatorname{fromCols}(A_1,A_2)=\operatorname{fromCols}(B_1,B_2) \iff A_1=B_1 \wedge A_2=B_2. $$$$

Lean4

@[simp]
theorem fromRows_mulVec [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) :
    fromRows A₁ A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) := by ext (_ | _) <;> rfl

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