Documentation

Mathlib.Data.Matrix.ColumnRowPartitioned

Block Matrices from Rows and Columns #

This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as A = fromCols A₁ A₂ the concatenation of two matrices with the same column indices can be expressed as B = fromRows B₁ B₂.

We then provide a few lemmas that deal with the products of these with each other and with block matrices

Tags #

column matrices, row matrices, column row block matrices

def Matrix.fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

Matrix (m₁ ⊕ m₂) n R

Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a bigger matrix indexed by [(m₁ ⊕ m₂) × N]

Equations

A₁.fromRows A₂ = Matrix.of (Sum.elim A₁ A₂)

def Matrix.fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :

Matrix m (n₁ ⊕ n₂) R

Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]

Equations

B₁.fromCols B₂ = Matrix.of fun (i : m) => Sum.elim (B₁ i) (B₂ i)

def Matrix.toCols₁ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :

Matrix m n₁ R

Given a column partitioned matrix extract the first column

Equations

A.toCols₁ = Matrix.of fun (i : m) (j : n₁) => A i (Sum.inl j)

def Matrix.toCols₂ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :

Matrix m n₂ R

Given a column partitioned matrix extract the second column

Equations

A.toCols₂ = Matrix.of fun (i : m) (j : n₂) => A i (Sum.inr j)

def Matrix.toRows₁ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :

Matrix m₁ n R

Given a row partitioned matrix extract the first row

Equations

A.toRows₁ = Matrix.of fun (i : m₁) (j : n) => A (Sum.inl i) j

def Matrix.toRows₂ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :

Matrix m₂ n R

Given a row partitioned matrix extract the second row

Equations

A.toRows₂ = Matrix.of fun (i : m₂) (j : n) => A (Sum.inr i) j

@[deprecated Matrix.fromCols (since := "2024-12-11")]

def Matrix.fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :

Matrix m (n₁ ⊕ n₂) R

Alias of Matrix.fromCols.

Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]

Equations

@Matrix.fromColumns = @Matrix.fromCols

@[deprecated Matrix.toCols₁ (since := "2024-12-11")]

def Matrix.toColumns₁ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :

Matrix m n₁ R

Alias of Matrix.toCols₁.

Given a column partitioned matrix extract the first column

Equations

@Matrix.toColumns₁ = @Matrix.toCols₁

@[deprecated Matrix.toCols₂ (since := "2024-12-11")]

def Matrix.toColumns₂ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :

Matrix m n₂ R

Alias of Matrix.toCols₂.

Given a column partitioned matrix extract the second column

Equations

@Matrix.toColumns₂ = @Matrix.toCols₂

@[simp]

theorem Matrix.fromRows_apply_inl {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₁) (j : n) :

A₁.fromRows A₂ (Sum.inl i) j = A₁ i j

@[simp]

theorem Matrix.fromRows_apply_inr {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₂) (j : n) :

A₁.fromRows A₂ (Sum.inr i) j = A₂ i j

@[simp]

theorem Matrix.fromCols_apply_inl {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :

A₁.fromCols A₂ i (Sum.inl j) = A₁ i j

@[deprecated Matrix.fromCols_apply_inl (since := "2024-12-11")]

theorem Matrix.fromColumns_apply_inl {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :

A₁.fromCols A₂ i (Sum.inl j) = A₁ i j

Alias of Matrix.fromCols_apply_inl.

@[simp]

theorem Matrix.fromCols_apply_inr {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :

A₁.fromCols A₂ i (Sum.inr j) = A₂ i j

@[deprecated Matrix.fromCols_apply_inr (since := "2024-12-11")]

theorem Matrix.fromColumns_apply_inr {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :

A₁.fromCols A₂ i (Sum.inr j) = A₂ i j

Alias of Matrix.fromCols_apply_inr.

@[simp]

theorem Matrix.toRows₁_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₁) (j : n) :

A.toRows₁ i j = A (Sum.inl i) j

@[simp]

theorem Matrix.toRows₂_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₂) (j : n) :

A.toRows₂ i j = A (Sum.inr i) j

@[simp]

theorem Matrix.toRows₁_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

(A₁.fromRows A₂).toRows₁ = A₁

@[simp]

theorem Matrix.toRows₂_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

(A₁.fromRows A₂).toRows₂ = A₂

@[simp]

theorem Matrix.toCols₁_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁) :

A.toCols₁ i j = A i (Sum.inl j)

@[deprecated Matrix.toCols₁_apply (since := "2024-12-11")]

theorem Matrix.toColumns₁_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁) :

A.toCols₁ i j = A i (Sum.inl j)

Alias of Matrix.toCols₁_apply.

@[simp]

theorem Matrix.toCols₂_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) :

A.toCols₂ i j = A i (Sum.inr j)

@[deprecated Matrix.toCols₂_apply (since := "2024-12-11")]

theorem Matrix.toColumns₂_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) :

A.toCols₂ i j = A i (Sum.inr j)

Alias of Matrix.toCols₂_apply.

@[simp]

theorem Matrix.toCols₁_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).toCols₁ = A₁

@[deprecated Matrix.toCols₁_fromCols (since := "2024-12-11")]

theorem Matrix.toColumns₁_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).toCols₁ = A₁

Alias of Matrix.toCols₁_fromCols.

@[simp]

theorem Matrix.toCols₂_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).toCols₂ = A₂

@[deprecated Matrix.toCols₂_fromCols (since := "2024-12-11")]

theorem Matrix.toColumns₂_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).toCols₂ = A₂

Alias of Matrix.toCols₂_fromCols.

@[simp]

theorem Matrix.fromCols_toCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :

A.toCols₁.fromCols A.toCols₂ = A

@[deprecated Matrix.fromCols_toCols (since := "2024-12-11")]

theorem Matrix.fromColumns_toColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :

A.toCols₁.fromCols A.toCols₂ = A

Alias of Matrix.fromCols_toCols.

@[simp]

theorem Matrix.fromRows_toRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :

A.toRows₁.fromRows A.toRows₂ = A

theorem Matrix.fromRows_inj {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} :

Function.Injective2 Matrix.fromRows

theorem Matrix.fromCols_inj {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} :

Function.Injective2 Matrix.fromCols

@[deprecated Matrix.fromCols_inj (since := "2024-12-11")]

theorem Matrix.fromColumns_inj {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} :

Function.Injective2 Matrix.fromCols

Alias of Matrix.fromCols_inj.

theorem Matrix.fromCols_ext_iff {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :

A₁.fromCols A₂ = B₁.fromCols B₂ ↔ A₁ = B₁ ∧ A₂ = B₂

@[deprecated Matrix.fromCols_ext_iff (since := "2024-12-11")]

theorem Matrix.fromColumns_ext_iff {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :

A₁.fromCols A₂ = B₁.fromCols B₂ ↔ A₁ = B₁ ∧ A₂ = B₂

Alias of Matrix.fromCols_ext_iff.

theorem Matrix.fromRows_ext_iff {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) :

A₁.fromRows A₂ = B₁.fromRows B₂ ↔ A₁ = B₁ ∧ A₂ = B₂

theorem Matrix.transpose_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).transpose = A₁.transpose.fromRows A₂.transpose

A column partitioned matrix when transposed gives a row partitioned matrix with columns of the initial matrix transposed to become rows.

@[deprecated Matrix.transpose_fromCols (since := "2024-12-11")]

theorem Matrix.transpose_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).transpose = A₁.transpose.fromRows A₂.transpose

Alias of Matrix.transpose_fromCols.

A column partitioned matrix when transposed gives a row partitioned matrix with columns of the initial matrix transposed to become rows.

theorem Matrix.transpose_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

(A₁.fromRows A₂).transpose = A₁.transpose.fromCols A₂.transpose

A row partitioned matrix when transposed gives a column partitioned matrix with rows of the initial matrix transposed to become columns.

@[simp]

theorem Matrix.fromRows_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

-A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

Negating a matrix partitioned by rows is equivalent to negating each of the rows.

@[simp]

theorem Matrix.fromCols_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :

-A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

Negating a matrix partitioned by columns is equivalent to negating each of the columns.

@[deprecated Matrix.fromCols_neg (since := "2024-12-11")]

theorem Matrix.fromColumns_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :

-A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

Alias of Matrix.fromCols_neg.

Negating a matrix partitioned by columns is equivalent to negating each of the columns.

@[simp]

theorem Matrix.fromCols_fromRows_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :

(B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

@[deprecated Matrix.fromCols_fromRows_eq_fromBlocks (since := "2024-12-11")]

theorem Matrix.fromColumns_fromRows_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :

(B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Alias of Matrix.fromCols_fromRows_eq_fromBlocks.

@[simp]

theorem Matrix.fromRows_fromCols_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :

(B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

@[deprecated Matrix.fromRows_fromCols_eq_fromBlocks (since := "2024-12-11")]

theorem Matrix.fromRows_fromColumn_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :

(B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Alias of Matrix.fromRows_fromCols_eq_fromBlocks.

@[simp]

theorem Matrix.fromRows_mulVec {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) :

(A₁.fromRows A₂).mulVec v = Sum.elim (A₁.mulVec v) (A₂.mulVec v)

@[simp]

theorem Matrix.vecMul_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :

Matrix.vecMul v (B₁.fromCols B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)

@[deprecated Matrix.vecMul_fromCols (since := "2024-12-11")]

theorem Matrix.vecMul_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :

Matrix.vecMul v (B₁.fromCols B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)

Alias of Matrix.vecMul_fromCols.

@[simp]

theorem Matrix.sum_elim_vecMul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁ → R) (v₂ : m₂ → R) :

Matrix.vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = Matrix.vecMul v₁ B₁ + Matrix.vecMul v₂ B₂

@[simp]

theorem Matrix.fromCols_mulVec_sum_elim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :

(A₁.fromCols A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂

@[deprecated Matrix.fromCols_mulVec_sum_elim (since := "2024-12-11")]

theorem Matrix.fromColumns_mulVec_sum_elim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :

(A₁.fromCols A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂

Alias of Matrix.fromCols_mulVec_sum_elim.

@[simp]

theorem Matrix.fromRows_mul {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :

A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)

@[simp]

theorem Matrix.mul_fromCols {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :

A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

@[deprecated Matrix.mul_fromCols (since := "2024-12-11")]

theorem Matrix.mul_fromColumns {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :

A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

Alias of Matrix.mul_fromCols.

@[simp]

theorem Matrix.fromRows_zero {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] :

Matrix.fromRows 0 0 = 0

@[simp]

theorem Matrix.fromCols_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] :

Matrix.fromCols 0 0 = 0

@[deprecated Matrix.fromCols_zero (since := "2024-12-11")]

theorem Matrix.fromColumns_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] :

Matrix.fromCols 0 0 = 0

Alias of Matrix.fromCols_zero.

theorem Matrix.fromRows_mul_fromCols {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :

A₁.fromRows A₂ * B₁.fromCols B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block matrix.

@[deprecated Matrix.fromRows_mul_fromCols (since := "2024-12-11")]

theorem Matrix.fromRows_mul_fromColumns {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :

A₁.fromRows A₂ * B₁.fromCols B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

Alias of Matrix.fromRows_mul_fromCols.

A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block matrix.

theorem Matrix.fromCols_mul_fromRows {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :

A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer" products of the block matrices.

@[deprecated Matrix.fromCols_mul_fromRows (since := "2024-12-11")]

theorem Matrix.fromColumns_mul_fromRows {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :

A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

Alias of Matrix.fromCols_mul_fromRows.

A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer" products of the block matrices.

theorem Matrix.fromCols_mul_fromBlocks {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :

A₁.fromCols A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

A column partitioned matrix multipiled by a block matrix results in a column partitioned matrix.

@[deprecated Matrix.fromCols_mul_fromBlocks (since := "2024-12-11")]

theorem Matrix.fromColumns_mul_fromBlocks {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :

A₁.fromCols A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

Alias of Matrix.fromCols_mul_fromBlocks.

A column partitioned matrix multipiled by a block matrix results in a column partitioned matrix.

theorem Matrix.fromBlocks_mul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :

Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix.

theorem Matrix.fromCols_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [CommRing R] [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂] (e : n ≃ n₁ ⊕ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :

A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

Multiplication of a matrix by its inverse is commutative. This is the column and row partitioned matrix form of Matrix.mul_eq_one_comm.

The condition e : n ≃ n₁ ⊕ n₂ states that fromCols A₁ A₂ and fromRows B₁ B₂ are "square".

@[deprecated Matrix.fromCols_mul_fromRows_eq_one_comm (since := "2024-12-11")]

theorem Matrix.fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [CommRing R] [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂] (e : n ≃ n₁ ⊕ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :

A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

Alias of Matrix.fromCols_mul_fromRows_eq_one_comm.

Multiplication of a matrix by its inverse is commutative. This is the column and row partitioned matrix form of Matrix.mul_eq_one_comm.

The condition e : n ≃ n₁ ⊕ n₂ states that fromCols A₁ A₂ and fromRows B₁ B₂ are "square".

theorem Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} [CommRing R] [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p] (A₁ : Matrix n { i : n // p i } R) (A₂ : Matrix n { i : n // ¬p i } R) (B₁ : Matrix { i : n // p i } n R) (B₂ : Matrix { i : n // ¬p i } n R) :

A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

The lemma fromCols_mul_fromRows_eq_one_comm specialized to the case where the index sets n₁ and n₂, are the result of subtyping by a predicate and its complement.

@[deprecated Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm (since := "2024-12-11")]

theorem Matrix.equiv_compl_fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} [CommRing R] [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p] (A₁ : Matrix n { i : n // p i } R) (A₂ : Matrix n { i : n // ¬p i } R) (B₁ : Matrix { i : n // p i } n R) (B₂ : Matrix { i : n // ¬p i } n R) :

A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

Alias of Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm.

The lemma fromCols_mul_fromRows_eq_one_comm specialized to the case where the index sets n₁ and n₂, are the result of subtyping by a predicate and its complement.

theorem Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Star R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose

A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned matrix with the columns of the initial matrix conjugate transposed to become rows.

@[deprecated Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose (since := "2024-12-11")]

theorem Matrix.conjTranspose_fromColumns_eq_fromRows_conjTranspose {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Star R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :

(A₁.fromCols A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose

Alias of Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose.

A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned matrix with the columns of the initial matrix conjugate transposed to become rows.

theorem Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Star R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

(A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromCols A₂.conjTranspose

A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix with the rows of the initial matrix conjugate transposed to become columns.

@[deprecated Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose (since := "2024-12-11")]

theorem Matrix.conjTranspose_fromRows_eq_fromColumns_conjTranspose {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Star R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :

(A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromCols A₂.conjTranspose

Alias of Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose.

A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix with the rows of the initial matrix conjugate transposed to become columns.