mul_fromCols — Mathlib

English

Multiplying a matrix A on the left by a concatenation fromCols B1 B2 distributes across the blocks: A * fromCols B1 B2 = fromCols (A * B1) (A * B2).

Русский

Умножение матрицы A слева на конкатенацию fromCols(B1,B2) распределяется по блочным частям: A * fromCols(B1,B2) = fromCols(A B1, A B2).

LaTeX

$$$$ A * fromCols(B_1,B_2) = fromCols(A B_1, A B_2). $$$$

Lean4

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

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