Matrix.fromColumns_mul_fromBlocks
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} [inst : Fintype m₁]
[inst_1 : Fintype m₂] [inst_2 : Semiring R] (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₁.fromColumns A₂ * B₁₁.fromBlocks B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromColumns (A₁ * B₁₂ + A₂ * B₂₂)
This theorem states that if we have a column partitioned matrix, represented by `A₁` and `A₂`, and a block matrix represented by `B₁₁`, `B₁₂`, `B₂₁`, `B₂₂` in a semiring `R`, then the result of multiplying the partitioned matrix by the block matrix is another column partitioned matrix. More specifically, the first column of the result is given by `A₁ * B₁₁ + A₂ * B₂₁`, and the second column is given by `A₁ * B₁₂ + A₂ * B₂₂`. The matrices' row indices are of types `m`, `m₁`, and `m₂`, and the column indices are of types `n₁` and `n₂`. The types `m₁` and `m₂` are assumed to be finite.
More concisely: Given column partitioned matrix `A₁` and `A₂` of sizes `m x (n₁ + n₂)` and block matrix `B₁₁`, `B₁₂`, `B₂₁`, `B₂₂` of size `(m₁ x p) x (q x n₁)` and `(m₂ x r) x (q x n₂)` in a semiring `R`, respectively, the product `A₁ * B₁₁ ⊎ A₂ * B₂₁ ⊎ A₁ * B₁₂ ⊎ A₂ * B₂₂` is a column partitioned matrix of size `m x (n₁ + n₂)` with first and second columns given by `A₁ * B₁₁ + A₂ * B₂₁` and `A₁ * B₁₂ + A₂ * B₂₂`, respectively.
|
Matrix.fromBlocks_mul_fromRows
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} [inst : Fintype n₁]
[inst_1 : Fintype n₂] [inst_2 : Semiring R] (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),
B₁₁.fromBlocks B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)
This theorem states that for any semiring `R` and any set of matrices `A₁`, `A₂`, `B₁₁`, `B₁₂`, `B₂₁`, `B₂₂` with appropriate dimensions, the product of a block matrix formed from `B₁₁`, `B₁₂`, `B₂₁`, `B₂₂` and a row-partitioned matrix formed from `A₁` and `A₂` is equal to a row partitioned matrix whose components are derived from the addition and multiplication operations on the individual components of the original matrices. Specifically, the new row-partitioned matrix's components are calculated as `(B₁₁ * A₁ + B₁₂ * A₂)` and `(B₂₁ * A₁ + B₂₂ * A₂)`. This is a statement about the compatibility of matrix multiplication with block and row-partitioned matrices.
More concisely: For any semiring `R` and matrices `A` partitioned into rows as `[A₁ | A₂]` and `B` partitioned into blocks as `[B₁₁ | B₁₂ ; B₂₁ | B₂₂]`, the product `B * [A₁ | A₂] = [B₁₁ * A₁ + B₁₂ * A₂ | B₂₁ * A₁ + B₂₂ * A₂]`.
|
Matrix.fromRows_mul_fromColumns
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} [inst : Fintype n]
[inst_1 : Semiring R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R),
A₁.fromRows A₂ * B₁.fromColumns B₂ = (A₁ * B₁).fromBlocks (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
This theorem states that for any semi-ring `R` and any types `m₁`, `m₂`, `n`, `n₁`, and `n₂`, given four matrices `A₁`, `A₂`, `B₁`, and `B₂`, where `A₁` and `A₂` have their rows indexed by `m₁` and `m₂` respectively and both have their columns indexed by `n`, and `B₁` and `B₂` have their rows indexed by `n` and their columns indexed by `n₁` and `n₂` respectively, the multiplication of a row partitioned matrix created from `A₁` and `A₂` and a column partitioned matrix created from `B₁` and `B₂` results in a 2 by 2 block matrix. This block matrix is formed by taking the blocks as the multiplication of `A₁` and `B₁`, `A₁` and `B₂`, `A₂` and `B₁`, and `A₂` and `B₂` respectively.
More concisely: Given matrices `A₁` and `A₂` with rows indexed by `m₁` and `m₂` respectively, columns indexed by `n`, and `B₁` and `B₂` with rows and columns indexed by `n`, `n₁`, and `n₂` respectively, the product of the row-partitioned matrices formed from `A₁`, `A₂`, `B₁`, and `B₂` is a 2 by 2 block matrix with blocks equal to the products of `A₁` and `B₁`, `A₁` and `B₂`, `A₂` and `B₁`, and `A₂` and `B₂`.
|
Matrix.fromColumns_mul_fromRows_eq_one_comm
theorem Matrix.fromColumns_mul_fromRows_eq_one_comm :
∀ {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Fintype n] [inst_1 : Fintype n₁]
[inst_2 : Fintype n₂] [inst_3 : DecidableEq n] [inst_4 : DecidableEq n₁] [inst_5 : DecidableEq n₂]
[inst_6 : CommRing R],
n ≃ n₁ ⊕ n₂ →
∀ (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R),
A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromColumns A₂ = 1
This theorem, named `Matrix.fromColumns_mul_fromRows_eq_one_comm`, states that for any commutative ring `R` and types `n`, `n₁`, and `n₂` (which can be indices for matrix rows or columns), given that `n` is equivalent to a disjoint sum of `n₁` and `n₂`, the matrix multiplication of matrices `A₁` and `A₂` (partitioned by columns) with matrices `B₁` and `B₂` (partitioned by rows) is commutative, if and only if the product of these matrices equals the identity matrix. This is a specific form of the more general property `Matrix.mul_eq_one_comm` tailored for partitioned matrices. The condition `n ≃ n₁ ⊕ n₂` ensures that the constructed matrices are square matrices, a necessary condition for the matrices to have an inverse.
More concisely: For any commutative ring R and square matrices A₁, A₂, B₁, and B₂ with compatible partitions by columns and rows, their matrix product is commutative if and only if A₁ * B₁ = B₂ * A₂ = I, where I is the identity matrix.
|
Matrix.fromColumns_mul_fromRows
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} [inst : Fintype n₁]
[inst_1 : Fintype n₂] [inst_2 : Semiring R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R)
(B₂ : Matrix n₂ n R), A₁.fromColumns A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂
The theorem `Matrix.fromColumns_mul_fromRows` states that for any finite types `n₁`, `n₂`, and for any semiring `R`, given any four matrices `A₁` and `A₂` of type `Matrix m n₁ R` and `Matrix m n₂ R` respectively, and `B₁` and `B₂` of type `Matrix n₁ n R` and `Matrix n₂ n R` respectively, the matrix product of `A₁.fromColumns A₂` and `B₁.fromRows B₂` is equal to the sum of the matrix products `A₁ * B₁` and `A₂ * B₂`. In other words, when a column-partitioned matrix is multiplied by a row-partitioned matrix, the resulting matrix is the sum of the "outer" products of the block matrices.
More concisely: For any semiring R and matrices A₁, A₂, B₁, and B₂ of compatible sizes over R, the product of column-partitioned matrix A₁ and row-partitioned matrix B₁ is equal to the sum of the matrices obtained by multiplying the corresponding block matrices A₁ and B₁, and A₂ and B₂.
|