fromRows_mul — Mathlib

English

Let A1, A2 be row-partitioned matrices and B a matrix that acts on the right. Then the product fromRows(A1,A2) * B equals fromRows(A1 * B, A2 * B).

Русский

Пусть A1, A2 — матрицы, разбиенные по строкам, и B — правая матрица. Тогда произведение fromRows(A1,A2) на B равно fromRows(A1 B, A2 B).

LaTeX

$$$$ \operatorname{fromRows}(A_1,A_2) \cdot B = \operatorname{fromRows}(A_1 B, A_2 B). $$$$

Lean4

@[simp]
theorem fromRows_mul [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
    fromRows A₁ A₂ * B = fromRows (A₁ * B) (A₂ * B) := by ext (_ | _) _ <;> simp [mul_apply]

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