# Block Matrices #

## Main definitions #

• Matrix.fromBlocks: build a block matrix out of 4 blocks
• Matrix.toBlocks₁₁, Matrix.toBlocks₁₂, Matrix.toBlocks₂₁, Matrix.toBlocks₂₂: extract each of the four blocks from Matrix.fromBlocks.
• Matrix.blockDiagonal: block diagonal of equally sized blocks. On square blocks, this is a ring homomorphisms, Matrix.blockDiagonalRingHom.
• Matrix.blockDiag: extract the blocks from the diagonal of a block diagonal matrix.
• Matrix.blockDiagonal': block diagonal of unequally sized blocks. On square blocks, this is a ring homomorphisms, Matrix.blockDiagonal'RingHom.
• Matrix.blockDiag': extract the blocks from the diagonal of a block diagonal matrix.
theorem Matrix.dotProduct_block {m : Type u_2} {n : Type u_3} {α : Type u_12} [] [] [Mul α] [] (v : m nα) (w : m nα) :
= Matrix.dotProduct (v Sum.inl) (w Sum.inl) + Matrix.dotProduct (v Sum.inr) (w Sum.inr)
def Matrix.fromBlocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
Matrix (n o) (l m) α

We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.

Equations
Instances For
@[simp]
theorem Matrix.fromBlocks_apply₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : n) (j : l) :
Matrix.fromBlocks A B C D () () = A i j
@[simp]
theorem Matrix.fromBlocks_apply₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : n) (j : m) :
Matrix.fromBlocks A B C D () () = B i j
@[simp]
theorem Matrix.fromBlocks_apply₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : o) (j : l) :
Matrix.fromBlocks A B C D () () = C i j
@[simp]
theorem Matrix.fromBlocks_apply₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : o) (j : m) :
Matrix.fromBlocks A B C D () () = D i j
def Matrix.toBlocks₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
Matrix n l α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top left" submatrix.

Equations
• = Matrix.of fun (i : n) (j : l) => M () ()
Instances For
def Matrix.toBlocks₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
Matrix n m α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top right" submatrix.

Equations
• = Matrix.of fun (i : n) (j : m) => M () ()
Instances For
def Matrix.toBlocks₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
Matrix o l α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom left" submatrix.

Equations
• = Matrix.of fun (i : o) (j : l) => M () ()
Instances For
def Matrix.toBlocks₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
Matrix o m α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom right" submatrix.

Equations
• = Matrix.of fun (i : o) (j : m) => M () ()
Instances For
theorem Matrix.fromBlocks_toBlocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
@[simp]
theorem Matrix.toBlocks_fromBlocks₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
@[simp]
theorem Matrix.toBlocks_fromBlocks₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
@[simp]
theorem Matrix.toBlocks_fromBlocks₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
@[simp]
theorem Matrix.toBlocks_fromBlocks₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
theorem Matrix.ext_iff_blocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {A : Matrix (n o) (l m) α} {B : Matrix (n o) (l m) α} :
A = B

Two block matrices are equal if their blocks are equal.

@[simp]
theorem Matrix.fromBlocks_inj {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {A : Matrix n l α} {B : Matrix n m α} {C : Matrix o l α} {D : Matrix o m α} {A' : Matrix n l α} {B' : Matrix n m α} {C' : Matrix o l α} {D' : Matrix o m α} :
= Matrix.fromBlocks A' B' C' D' A = A' B = B' C = C' D = D'
theorem Matrix.fromBlocks_map {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : αβ) :
Matrix.map () f = Matrix.fromBlocks () () () ()
theorem Matrix.fromBlocks_transpose {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
theorem Matrix.fromBlocks_conjTranspose {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Star α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
@[simp]
theorem Matrix.fromBlocks_submatrix_sum_swap_left {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : pl m) :
Matrix.submatrix () Sum.swap f = Matrix.submatrix () id f
@[simp]
theorem Matrix.fromBlocks_submatrix_sum_swap_right {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : pn o) :
Matrix.submatrix () f Sum.swap = Matrix.submatrix () f id
theorem Matrix.fromBlocks_submatrix_sum_swap_sum_swap {l : Type u_14} {m : Type u_15} {n : Type u_16} {o : Type u_17} {α : Type u_18} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
Matrix.submatrix () Sum.swap Sum.swap =
def Matrix.IsTwoBlockDiagonal {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] (A : Matrix (n o) (l m) α) :

A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish

Equations
Instances For
def Matrix.toBlock {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : Matrix m n α) (p : mProp) (q : nProp) :
Matrix { a : m // p a } { a : n // q a } α

Let p pick out certain rows and q pick out certain columns of a matrix M. Then toBlock M p q is the corresponding block matrix.

Equations
Instances For
@[simp]
theorem Matrix.toBlock_apply {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : Matrix m n α) (p : mProp) (q : nProp) (i : { a : m // p a }) (j : { a : n // q a }) :
Matrix.toBlock M p q i j = M i j
def Matrix.toSquareBlockProp {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : mProp) :
Matrix { a : m // p a } { a : m // p a } α

Let p pick out certain rows and columns of a square matrix M. Then toSquareBlockProp M p is the corresponding block matrix.

Equations
Instances For
theorem Matrix.toSquareBlockProp_def {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : mProp) :
= Matrix.of fun (i j : { a : m // p a }) => M i j
def Matrix.toSquareBlock {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : Matrix m m α) (b : mβ) (k : β) :
Matrix { a : m // b a = k } { a : m // b a = k } α

Let b map rows and columns of a square matrix M to blocks. Then toSquareBlock M b k is the block k matrix.

Equations
Instances For
theorem Matrix.toSquareBlock_def {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : Matrix m m α) (b : mβ) (k : β) :
= Matrix.of fun (i j : { a : m // b a = k }) => M i j
theorem Matrix.fromBlocks_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_10} {α : Type u_12} [SMul R α] (x : R) (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
x = Matrix.fromBlocks (x A) (x B) (x C) (x D)
theorem Matrix.fromBlocks_neg {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_10} [Neg R] (A : Matrix n l R) (B : Matrix n m R) (C : Matrix o l R) (D : Matrix o m R) :
- = Matrix.fromBlocks (-A) (-B) (-C) (-D)
@[simp]
theorem Matrix.fromBlocks_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] :
= 0
theorem Matrix.fromBlocks_add {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Add α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix n l α) (B' : Matrix n m α) (C' : Matrix o l α) (D' : Matrix o m α) :
+ Matrix.fromBlocks A' B' C' D' = Matrix.fromBlocks (A + A') (B + B') (C + C') (D + D')
theorem Matrix.fromBlocks_multiply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {q : Type u_6} {α : Type u_12} [] [] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix l p α) (B' : Matrix l q α) (C' : Matrix m p α) (D' : Matrix m q α) :
* Matrix.fromBlocks A' B' C' D' = Matrix.fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')
theorem Matrix.fromBlocks_mulVec {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : l mα) :
Matrix.mulVec () x = Sum.elim (Matrix.mulVec A (x Sum.inl) + Matrix.mulVec B (x Sum.inr)) (Matrix.mulVec C (x Sum.inl) + Matrix.mulVec D (x Sum.inr))
theorem Matrix.vecMul_fromBlocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : n oα) :
Matrix.vecMul x () = Sum.elim (Matrix.vecMul (x Sum.inl) A + Matrix.vecMul (x Sum.inr) C) (Matrix.vecMul (x Sum.inl) B + Matrix.vecMul (x Sum.inr) D)
theorem Matrix.toBlock_diagonal_self {m : Type u_2} {α : Type u_12} [] [Zero α] (d : mα) (p : mProp) :
= Matrix.diagonal fun (i : ) => d i
theorem Matrix.toBlock_diagonal_disjoint {m : Type u_2} {α : Type u_12} [] [Zero α] (d : mα) {p : mProp} {q : mProp} (hpq : Disjoint p q) :
= 0
@[simp]
theorem Matrix.fromBlocks_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [] [] [Zero α] (d₁ : lα) (d₂ : mα) :
@[simp]
theorem Matrix.toBlocks₁₁_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [] [] [Zero α] (v : l mα) :
= Matrix.diagonal fun (i : l) => v ()
@[simp]
theorem Matrix.toBlocks₂₂_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [] [] [Zero α] (v : l mα) :
= Matrix.diagonal fun (i : m) => v ()
@[simp]
theorem Matrix.toBlocks₁₂_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [] [] [Zero α] (v : l mα) :
@[simp]
theorem Matrix.toBlocks₂₁_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [] [] [Zero α] (v : l mα) :
@[simp]
theorem Matrix.fromBlocks_one {l : Type u_1} {m : Type u_2} {α : Type u_12} [] [] [Zero α] [One α] :
= 1
@[simp]
theorem Matrix.toBlock_one_self {m : Type u_2} {α : Type u_12} [] [Zero α] [One α] (p : mProp) :
= 1
theorem Matrix.toBlock_one_disjoint {m : Type u_2} {α : Type u_12} [] [Zero α] [One α] {p : mProp} {q : mProp} (hpq : Disjoint p q) :
= 0
def Matrix.blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) :
Matrix (m × o) (n × o) α

Matrix.blockDiagonal M turns a homogenously-indexed collection of matrices M : o → Matrix m n α' into an m × o-by-n × o block matrix which has the entries of M along the diagonal and zero elsewhere.

See also Matrix.blockDiagonal' if the matrices may not have the same size everywhere.

Equations
• = Matrix.of fun (x : m × o) (x_1 : n × o) => match x with | (i, k) => match x_1 with | (j, k') => if k = k' then M k i j else 0
Instances For
theorem Matrix.blockDiagonal_apply' {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) (i : m) (k : o) (j : n) (k' : o) :
Matrix.blockDiagonal M (i, k) (j, k') = if k = k' then M k i j else 0
theorem Matrix.blockDiagonal_apply {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) (ik : m × o) (jk : n × o) :
Matrix.blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0
@[simp]
theorem Matrix.blockDiagonal_apply_eq {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) (i : m) (j : n) (k : o) :
Matrix.blockDiagonal M (i, k) (j, k) = M k i j
theorem Matrix.blockDiagonal_apply_ne {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) (i : m) (j : n) {k : o} {k' : o} (h : k k') :
Matrix.blockDiagonal M (i, k) (j, k') = 0
theorem Matrix.blockDiagonal_map {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} [] [Zero α] [Zero β] (M : oMatrix m n α) (f : αβ) (hf : f 0 = 0) :
= Matrix.blockDiagonal fun (k : o) => Matrix.map (M k) f
@[simp]
theorem Matrix.blockDiagonal_transpose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) :
@[simp]
theorem Matrix.blockDiagonal_conjTranspose {m : Type u_2} {n : Type u_3} {o : Type u_4} [] {α : Type u_14} [] [] (M : oMatrix m n α) :
@[simp]
theorem Matrix.blockDiagonal_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] :
@[simp]
theorem Matrix.blockDiagonal_diagonal {m : Type u_2} {o : Type u_4} {α : Type u_12} [] [Zero α] [] (d : omα) :
(Matrix.blockDiagonal fun (k : o) => Matrix.diagonal (d k)) = Matrix.diagonal fun (ik : m × o) => d ik.2 ik.1
@[simp]
theorem Matrix.blockDiagonal_one {m : Type u_2} {o : Type u_4} {α : Type u_12} [] [Zero α] [] [One α] :
@[simp]
theorem Matrix.blockDiagonal_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [] (M : oMatrix m n α) (N : oMatrix m n α) :
@[simp]
theorem Matrix.blockDiagonalAddMonoidHom_apply (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [] [] (M : oMatrix m n α) :
() M =
def Matrix.blockDiagonalAddMonoidHom (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [] [] :
(oMatrix m n α) →+ Matrix (m × o) (n × o) α

Matrix.blockDiagonal as an AddMonoidHom.

Equations
• = { toZeroHom := { toFun := Matrix.blockDiagonal, map_zero' := }, map_add' := }
Instances For
@[simp]
theorem Matrix.blockDiagonal_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [] (M : oMatrix m n α) :
@[simp]
theorem Matrix.blockDiagonal_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [] (M : oMatrix m n α) (N : oMatrix m n α) :
@[simp]
theorem Matrix.blockDiagonal_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} [] [] [] (M : oMatrix m n α) (N : oMatrix n p α) :
(Matrix.blockDiagonal fun (k : o) => M k * N k) =
@[simp]
theorem Matrix.blockDiagonalRingHom_apply (m : Type u_2) (o : Type u_4) (α : Type u_12) [] [] [] [] [] (M : oMatrix m m α) :
() M =
def Matrix.blockDiagonalRingHom (m : Type u_2) (o : Type u_4) (α : Type u_12) [] [] [] [] [] :
(oMatrix m m α) →+* Matrix (m × o) (m × o) α

Matrix.blockDiagonal as a RingHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Matrix.blockDiagonal_pow {m : Type u_2} {o : Type u_4} {α : Type u_12} [] [] [] [] [] (M : oMatrix m m α) (n : ) :
@[simp]
theorem Matrix.blockDiagonal_smul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] {R : Type u_14} [] [] [] (x : R) (M : oMatrix m n α) :
def Matrix.blockDiag {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o) :
Matrix m n α

Extract a block from the diagonal of a block diagonal matrix.

This is the block form of Matrix.diag, and the left-inverse of Matrix.blockDiagonal.

Equations
• = Matrix.of fun (i : m) (j : n) => M (i, k) (j, k)
Instances For
theorem Matrix.blockDiag_apply {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o) (i : m) (j : n) :
Matrix.blockDiag M k i j = M (i, k) (j, k)
theorem Matrix.blockDiag_map {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (M : Matrix (m × o) (n × o) α) (f : αβ) :
= fun (k : o) => Matrix.map () f
@[simp]
theorem Matrix.blockDiag_transpose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o) :
@[simp]
theorem Matrix.blockDiag_conjTranspose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_14} [] [] (M : Matrix (m × o) (n × o) α) (k : o) :
@[simp]
theorem Matrix.blockDiag_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] :
@[simp]
theorem Matrix.blockDiag_diagonal {m : Type u_2} {o : Type u_4} {α : Type u_12} [Zero α] [] [] (d : m × oα) (k : o) :
= Matrix.diagonal fun (i : m) => d (i, k)
@[simp]
theorem Matrix.blockDiag_blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] [] (M : oMatrix m n α) :
theorem Matrix.blockDiagonal_injective {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] [] :
Function.Injective Matrix.blockDiagonal
@[simp]
theorem Matrix.blockDiagonal_inj {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] [] {M : oMatrix m n α} {N : oMatrix m n α} :
@[simp]
theorem Matrix.blockDiag_one {m : Type u_2} {o : Type u_4} {α : Type u_12} [Zero α] [] [] [One α] :
@[simp]
theorem Matrix.blockDiag_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] (M : Matrix (m × o) (n × o) α) (N : Matrix (m × o) (n × o) α) :
@[simp]
theorem Matrix.blockDiagAddMonoidHom_apply (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [] (M : Matrix (m × o) (n × o) α) (k : o) :
() M k =
def Matrix.blockDiagAddMonoidHom (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [] :
Matrix (m × o) (n × o) α →+ oMatrix m n α

Matrix.blockDiag as an AddMonoidHom.

Equations
• = { toZeroHom := { toFun := Matrix.blockDiag, map_zero' := }, map_add' := }
Instances For
@[simp]
theorem Matrix.blockDiag_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] (M : Matrix (m × o) (n × o) α) :
@[simp]
theorem Matrix.blockDiag_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] (M : Matrix (m × o) (n × o) α) (N : Matrix (m × o) (n × o) α) :
@[simp]
theorem Matrix.blockDiag_smul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {R : Type u_14} [] [] [] (x : R) (M : Matrix (m × o) (n × o) α) :
def Matrix.blockDiagonal' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) :
Matrix ((i : o) × m' i) ((i : o) × n' i) α

Matrix.blockDiagonal' M turns M : Π i, Matrix (m i) (n i) α into a Σ i, m i-by-Σ i, n i block matrix which has the entries of M along the diagonal and zero elsewhere.

This is the dependently-typed version of Matrix.blockDiagonal.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Matrix.blockDiagonal'_apply' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (k' : o) (j : n' k') :
Matrix.blockDiagonal' M { fst := k, snd := i } { fst := k', snd := j } = if h : k = k' then M k i (cast j) else 0
theorem Matrix.blockDiagonal'_eq_blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) {k : o} {k' : o} (i : m) (j : n) :
Matrix.blockDiagonal M (i, k) (j, k') = Matrix.blockDiagonal' M { fst := k, snd := i } { fst := k', snd := j }
theorem Matrix.blockDiagonal'_submatrix_eq_blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [] [Zero α] (M : oMatrix m n α) :
Matrix.submatrix (Prod.toSigma Prod.swap) (Prod.toSigma Prod.swap) =
theorem Matrix.blockDiagonal'_apply {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (ik : (i : o) × m' i) (jk : (i : o) × n' i) :
= if h : ik.fst = jk.fst then M ik.fst ik.snd (cast jk.snd) else 0
@[simp]
theorem Matrix.blockDiagonal'_apply_eq {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (j : n' k) :
Matrix.blockDiagonal' M { fst := k, snd := i } { fst := k, snd := j } = M k i j
theorem Matrix.blockDiagonal'_apply_ne {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) {k : o} {k' : o} (i : m' k) (j : n' k') (h : k k') :
Matrix.blockDiagonal' M { fst := k, snd := i } { fst := k', snd := j } = 0
theorem Matrix.blockDiagonal'_map {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} {β : Type u_13} [] [Zero α] [Zero β] (M : (i : o) → Matrix (m' i) (n' i) α) (f : αβ) (hf : f 0 = 0) :
= Matrix.blockDiagonal' fun (k : o) => Matrix.map (M k) f
@[simp]
theorem Matrix.blockDiagonal'_transpose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) :
@[simp]
theorem Matrix.blockDiagonal'_conjTranspose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} [] {α : Type u_14} [] [] (M : (i : o) → Matrix (m' i) (n' i) α) :
@[simp]
theorem Matrix.blockDiagonal'_zero {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [Zero α] :
@[simp]
theorem Matrix.blockDiagonal'_diagonal {o : Type u_4} {m' : oType u_7} {α : Type u_12} [] [Zero α] [(i : o) → DecidableEq (m' i)] (d : (i : o) → m' iα) :
(Matrix.blockDiagonal' fun (k : o) => Matrix.diagonal (d k)) = Matrix.diagonal fun (ik : (i : o) × m' i) => d ik.fst ik.snd
@[simp]
theorem Matrix.blockDiagonal'_one {o : Type u_4} {m' : oType u_7} {α : Type u_12} [] [Zero α] [(i : o) → DecidableEq (m' i)] [One α] :
@[simp]
theorem Matrix.blockDiagonal'_add {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [] (M : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (m' i) (n' i) α) :
@[simp]
theorem Matrix.blockDiagonal'AddMonoidHom_apply {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [] [] (M : (i : o) → Matrix (m' i) (n' i) α) :
() M =
def Matrix.blockDiagonal'AddMonoidHom {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [] [] :
((i : o) → Matrix (m' i) (n' i) α) →+ Matrix ((i : o) × m' i) ((i : o) × n' i) α

Matrix.blockDiagonal' as an AddMonoidHom.

Equations
• = { toZeroHom := { toFun := Matrix.blockDiagonal', map_zero' := }, map_add' := }
Instances For
@[simp]
theorem Matrix.blockDiagonal'_neg {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [] (M : (i : o) → Matrix (m' i) (n' i) α) :
@[simp]
theorem Matrix.blockDiagonal'_sub {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] [] (M : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (m' i) (n' i) α) :
@[simp]
theorem Matrix.blockDiagonal'_mul {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {p' : oType u_9} {α : Type u_12} [] [(i : o) → Fintype (n' i)] [] (M : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (n' i) (p' i) α) :
(Matrix.blockDiagonal' fun (k : o) => M k * N k) =
@[simp]
theorem Matrix.blockDiagonal'RingHom_apply {o : Type u_4} (m' : oType u_7) (α : Type u_12) [] [(i : o) → DecidableEq (m' i)] [] [(i : o) → Fintype (m' i)] [] (M : (i : o) → Matrix (m' i) (m' i) α) :
def Matrix.blockDiagonal'RingHom {o : Type u_4} (m' : oType u_7) (α : Type u_12) [] [(i : o) → DecidableEq (m' i)] [] [(i : o) → Fintype (m' i)] [] :
((i : o) → Matrix (m' i) (m' i) α) →+* Matrix ((i : o) × m' i) ((i : o) × m' i) α

Matrix.blockDiagonal' as a RingHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Matrix.blockDiagonal'_pow {o : Type u_4} {m' : oType u_7} {α : Type u_12} [] [(i : o) → DecidableEq (m' i)] [] [(i : o) → Fintype (m' i)] [] (M : (i : o) → Matrix (m' i) (m' i) α) (n : ) :
@[simp]
theorem Matrix.blockDiagonal'_smul {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] {R : Type u_14} [] [] [Module R α] (x : R) (M : (i : o) → Matrix (m' i) (n' i) α) :
def Matrix.blockDiag' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
Matrix (m' k) (n' k) α

Extract a block from the diagonal of a block diagonal matrix.

This is the block form of Matrix.diag, and the left-inverse of Matrix.blockDiagonal'.

Equations
• = Matrix.of fun (i : m' k) (j : n' k) => M { fst := k, snd := i } { fst := k, snd := j }
Instances For
theorem Matrix.blockDiag'_apply {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) (i : m' k) (j : n' k) :
= M { fst := k, snd := i } { fst := k, snd := j }
theorem Matrix.blockDiag'_map {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} {β : Type u_13} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (f : αβ) :
= fun (k : o) => Matrix.map () f
@[simp]
theorem Matrix.blockDiag'_transpose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
@[simp]
theorem Matrix.blockDiag'_conjTranspose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_14} [] [] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
@[simp]
theorem Matrix.blockDiag'_zero {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] :
@[simp]
theorem Matrix.blockDiag'_diagonal {o : Type u_4} {m' : oType u_7} {α : Type u_12} [Zero α] [] [(i : o) → DecidableEq (m' i)] (d : (i : o) × m' iα) (k : o) :
= Matrix.diagonal fun (i : m' k) => d { fst := k, snd := i }
@[simp]
theorem Matrix.blockDiag'_blockDiagonal' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] [] (M : (i : o) → Matrix (m' i) (n' i) α) :
theorem Matrix.blockDiagonal'_injective {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] [] :
Function.Injective Matrix.blockDiagonal'
@[simp]
theorem Matrix.blockDiagonal'_inj {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] [] {M : (i : o) → Matrix (m' i) (n' i) α} {N : (i : o) → Matrix (m' i) (n' i) α} :
@[simp]
theorem Matrix.blockDiag'_one {o : Type u_4} {m' : oType u_7} {α : Type u_12} [Zero α] [] [(i : o) → DecidableEq (m' i)] [One α] :
@[simp]
theorem Matrix.blockDiag'_add {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
@[simp]
theorem Matrix.blockDiag'AddMonoidHom_apply {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
() M k =
def Matrix.blockDiag'AddMonoidHom {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [] :
Matrix ((i : o) × m' i) ((i : o) × n' i) α →+ (i : o) → Matrix (m' i) (n' i) α

Matrix.blockDiag' as an AddMonoidHom.

Equations
• = { toZeroHom := { toFun := Matrix.blockDiag', map_zero' := }, map_add' := }
Instances For
@[simp]
theorem Matrix.blockDiag'_neg {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
@[simp]
theorem Matrix.blockDiag'_sub {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
@[simp]
theorem Matrix.blockDiag'_smul {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} {R : Type u_14} [] [] [] (x : R) (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
theorem Matrix.toBlock_mul_eq_mul {R : Type u_10} [] {m : Type u_14} {n : Type u_15} {k : Type u_16} [] (p : mProp) (q : kProp) (A : Matrix m n R) (B : Matrix n k R) :
Matrix.toBlock (A * B) p q = *
theorem Matrix.toBlock_mul_eq_add {R : Type u_10} [] {m : Type u_14} {n : Type u_15} {k : Type u_16} [] (p : mProp) (q : nProp) [] (r : kProp) (A : Matrix m n R) (B : Matrix n k R) :
Matrix.toBlock (A * B) p r = * + (Matrix.toBlock A p fun (i : n) => ¬q i) * Matrix.toBlock B (fun (i : n) => ¬q i) r