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} [Fintype m] [Fintype n] [Mul α] [AddCommMonoid α] (v w : m ⊕ n → α) : v ⬝ᵥ w = v ∘ Sum.inl ⬝ᵥ w ∘ Sum.inl + 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

• Matrix.fromBlocks A B C D = Matrix.of (Sum.elim (fun (i : n) => Sum.elim (A i) (B i)) fun (j : o) => Sum.elim (C j) (D 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 : l) : Matrix.fromBlocks A B C D (Sum.inl i) (Sum.inl j) = 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 (Sum.inl i) (Sum.inr j) = 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 (Sum.inr i) (Sum.inl j) = 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 (Sum.inr i) (Sum.inr j) = 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

• M.toBlocks₁₁ = Matrix.of fun (i : n) (j : l) => M (Sum.inl i) (Sum.inl 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 m α

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

Equations

• M.toBlocks₁₂ = Matrix.of fun (i : n) (j : m) => M (Sum.inl i) (Sum.inr 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 o l α

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

Equations

• M.toBlocks₂₁ = Matrix.of fun (i : o) (j : l) => M (Sum.inr i) (Sum.inl 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 o m α

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

Equations

• M.toBlocks₂₂ = Matrix.of fun (i : o) (j : m) => M (Sum.inr i) (Sum.inr j)

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) α) : Matrix.fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = 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 α) : (Matrix.fromBlocks A B C D).toBlocks₁₁ = A

@[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 α) : (Matrix.fromBlocks A B C D).toBlocks₁₂ = B

@[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 α) : (Matrix.fromBlocks A B C D).toBlocks₂₁ = C

@[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 α) : (Matrix.fromBlocks A B C D).toBlocks₂₂ = D

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 B : Matrix (n ⊕ o) (l ⊕ m) α} : A = B ↔ A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂

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 = 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.fromBlocks A B C D).map f = Matrix.fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)

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 α) : (Matrix.fromBlocks A B C D).transpose = Matrix.fromBlocks A.transpose C.transpose B.transpose D.transpose

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 α) : (Matrix.fromBlocks A B C D).conjTranspose = Matrix.fromBlocks A.conjTranspose C.conjTranspose B.conjTranspose D.conjTranspose

@[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 : p → l ⊕ m) : (Matrix.fromBlocks A B C D).submatrix Sum.swap f = (Matrix.fromBlocks C D A B).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 : p → n ⊕ o) : (Matrix.fromBlocks A B C D).submatrix f Sum.swap = (Matrix.fromBlocks B A D C).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.fromBlocks A B C D).submatrix Sum.swap Sum.swap = Matrix.fromBlocks D C B A

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) α) : Prop

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

Equations

• A.IsTwoBlockDiagonal = (A.toBlocks₁₂ = 0 ∧ A.toBlocks₂₁ = 0)

def Matrix.toBlock {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : Matrix m n α) (p : m → Prop) (q : n → Prop) : 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

• M.toBlock p q = M.submatrix Subtype.val Subtype.val

@[simp]

theorem Matrix.toBlock_apply {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : Matrix m n α) (p : m → Prop) (q : n → Prop) (i : { a : m // p a }) (j : { a : n // q a }) : M.toBlock p q i j = M ↑i ↑j

def Matrix.toSquareBlockProp {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : m → Prop) : 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

• M.toSquareBlockProp p = M.toBlock p p

theorem Matrix.toSquareBlockProp_def {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : m → Prop) : M.toSquareBlockProp p = 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

• M.toSquareBlock b k = M.toSquareBlockProp fun (a : m) => b a = k

theorem Matrix.toSquareBlock_def {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : Matrix m m α) (b : m → β) (k : β) : M.toSquareBlock b 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 A B C D = 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 = 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 α] : Matrix.fromBlocks 0 0 0 0 = 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' 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} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (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' 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} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : l ⊕ m → α) : (Matrix.fromBlocks A B C D).mulVec x = Sum.elim (A.mulVec (x ∘ Sum.inl) + B.mulVec (x ∘ Sum.inr)) (C.mulVec (x ∘ Sum.inl) + D.mulVec (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} [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : n ⊕ o → α) : Matrix.vecMul x (Matrix.fromBlocks A B C D) = 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} [DecidableEq m] [Zero α] (d : m → α) (p : m → Prop) : (Matrix.diagonal d).toBlock p p = Matrix.diagonal fun (i : Subtype p) => d ↑i

theorem Matrix.toBlock_diagonal_disjoint {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] (d : m → α) {p q : m → Prop} (hpq : Disjoint p q) : (Matrix.diagonal d).toBlock p q = 0

@[simp]

theorem Matrix.fromBlocks_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (d₁ : l → α) (d₂ : m → α) : Matrix.fromBlocks (Matrix.diagonal d₁) 0 0 (Matrix.diagonal d₂) = Matrix.diagonal (Sum.elim d₁ d₂)

@[simp]

theorem Matrix.toBlocks₁₁_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l ⊕ m → α) : (Matrix.diagonal v).toBlocks₁₁ = Matrix.diagonal fun (i : l) => v (Sum.inl i)

@[simp]

theorem Matrix.toBlocks₂₂_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l ⊕ m → α) : (Matrix.diagonal v).toBlocks₂₂ = Matrix.diagonal fun (i : m) => v (Sum.inr i)

@[simp]

theorem Matrix.toBlocks₁₂_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l ⊕ m → α) : (Matrix.diagonal v).toBlocks₁₂ = 0

@[simp]

theorem Matrix.toBlocks₂₁_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l ⊕ m → α) : (Matrix.diagonal v).toBlocks₂₁ = 0

@[simp]

theorem Matrix.fromBlocks_one {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] [One α] : Matrix.fromBlocks 1 0 0 1 = 1

@[simp]

theorem Matrix.toBlock_one_self {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] [One α] (p : m → Prop) : Matrix.toBlock 1 p p = 1

theorem Matrix.toBlock_one_disjoint {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] [One α] {p q : m → Prop} (hpq : Disjoint p q) : Matrix.toBlock 1 p q = 0

def Matrix.blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : o → Matrix 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.blockDiagonal M = 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

theorem Matrix.blockDiagonal_apply' {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : o → Matrix 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} [DecidableEq o] [Zero α] (M : o → Matrix 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} [DecidableEq o] [Zero α] (M : o → Matrix 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} [DecidableEq o] [Zero α] (M : o → Matrix m n α) (i : m) (j : n) {k 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} [DecidableEq o] [Zero α] [Zero β] (M : o → Matrix m n α) (f : α → β) (hf : f 0 = 0) : (Matrix.blockDiagonal M).map f = Matrix.blockDiagonal fun (k : o) => (M k).map f

@[simp]

theorem Matrix.blockDiagonal_transpose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : o → Matrix m n α) : (Matrix.blockDiagonal M).transpose = Matrix.blockDiagonal fun (k : o) => (M k).transpose

@[simp]

theorem Matrix.blockDiagonal_conjTranspose {m : Type u_2} {n : Type u_3} {o : Type u_4} [DecidableEq o] {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : o → Matrix m n α) : (Matrix.blockDiagonal M).conjTranspose = Matrix.blockDiagonal fun (k : o) => (M k).conjTranspose

@[simp]

theorem Matrix.blockDiagonal_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] : Matrix.blockDiagonal 0 = 0

@[simp]

theorem Matrix.blockDiagonal_diagonal {m : Type u_2} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] [DecidableEq m] (d : o → m → α) : (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} [DecidableEq o] [Zero α] [DecidableEq m] [One α] : Matrix.blockDiagonal 1 = 1

@[simp]

theorem Matrix.blockDiagonal_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [AddZeroClass α] (M N : o → Matrix m n α) : Matrix.blockDiagonal (M + N) = Matrix.blockDiagonal M + Matrix.blockDiagonal N

def Matrix.blockDiagonalAddMonoidHom (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [DecidableEq o] [AddZeroClass α] : (o → Matrix m n α) →+ Matrix (m × o) (n × o) α

Matrix.blockDiagonal as an AddMonoidHom.

Equations

• Matrix.blockDiagonalAddMonoidHom m n o α = { toFun := Matrix.blockDiagonal, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.blockDiagonalAddMonoidHom_apply (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [DecidableEq o] [AddZeroClass α] (M : o → Matrix m n α) : (Matrix.blockDiagonalAddMonoidHom m n o α) M = Matrix.blockDiagonal M

@[simp]

theorem Matrix.blockDiagonal_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [AddGroup α] (M : o → Matrix m n α) : Matrix.blockDiagonal (-M) = -Matrix.blockDiagonal M

@[simp]

theorem Matrix.blockDiagonal_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [AddGroup α] (M N : o → Matrix m n α) : Matrix.blockDiagonal (M - N) = Matrix.blockDiagonal M - Matrix.blockDiagonal 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} [DecidableEq o] [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : o → Matrix m n α) (N : o → Matrix n p α) : (Matrix.blockDiagonal fun (k : o) => M k * N k) = Matrix.blockDiagonal M * Matrix.blockDiagonal N

def Matrix.blockDiagonalRingHom (m : Type u_2) (o : Type u_4) (α : Type u_12) [DecidableEq o] [DecidableEq m] [Fintype o] [Fintype m] [NonAssocSemiring α] : (o → Matrix m m α) →+* Matrix (m × o) (m × o) α

Matrix.blockDiagonal as a RingHom.

Equations

• Matrix.blockDiagonalRingHom m o α = { toFun := Matrix.blockDiagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.blockDiagonalRingHom_apply (m : Type u_2) (o : Type u_4) (α : Type u_12) [DecidableEq o] [DecidableEq m] [Fintype o] [Fintype m] [NonAssocSemiring α] (M : o → Matrix m m α) : (Matrix.blockDiagonalRingHom m o α) M = Matrix.blockDiagonal M

@[simp]

theorem Matrix.blockDiagonal_pow {m : Type u_2} {o : Type u_4} {α : Type u_12} [DecidableEq o] [DecidableEq m] [Fintype o] [Fintype m] [Semiring α] (M : o → Matrix m m α) (n : ℕ) : Matrix.blockDiagonal (M ^ n) = Matrix.blockDiagonal M ^ n

@[simp]

theorem Matrix.blockDiagonal_smul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] {R : Type u_14} [Monoid R] [AddMonoid α] [DistribMulAction R α] (x : R) (M : o → Matrix m n α) : Matrix.blockDiagonal (x • M) = x • Matrix.blockDiagonal M

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

• M.blockDiag k = Matrix.of fun (i : m) (j : n) => M (i, k) (j, k)

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) : M.blockDiag 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 : α → β) : (M.map f).blockDiag = fun (k : o) => (M.blockDiag k).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) : M.transpose.blockDiag k = (M.blockDiag k).transpose

@[simp]

theorem Matrix.blockDiag_conjTranspose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : Matrix (m × o) (n × o) α) (k : o) : M.conjTranspose.blockDiag k = (M.blockDiag k).conjTranspose

@[simp]

theorem Matrix.blockDiag_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] : Matrix.blockDiag 0 = 0

@[simp]

theorem Matrix.blockDiag_diagonal {m : Type u_2} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] [DecidableEq m] (d : m × o → α) (k : o) : (Matrix.diagonal d).blockDiag k = 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 α] [DecidableEq o] (M : o → Matrix m n α) : (Matrix.blockDiagonal M).blockDiag = M

theorem Matrix.blockDiagonal_injective {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] : 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 α] [DecidableEq o] {M N : o → Matrix m n α} : Matrix.blockDiagonal M = Matrix.blockDiagonal N ↔ M = N

@[simp]

theorem Matrix.blockDiag_one {m : Type u_2} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] [DecidableEq m] [One α] : Matrix.blockDiag 1 = 1

@[simp]

theorem Matrix.blockDiag_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [AddZeroClass α] (M N : Matrix (m × o) (n × o) α) : (M + N).blockDiag = M.blockDiag + N.blockDiag

def Matrix.blockDiagAddMonoidHom (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [AddZeroClass α] : Matrix (m × o) (n × o) α →+ o → Matrix m n α

Matrix.blockDiag as an AddMonoidHom.

Equations

• Matrix.blockDiagAddMonoidHom m n o α = { toFun := Matrix.blockDiag, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.blockDiagAddMonoidHom_apply (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [AddZeroClass α] (M : Matrix (m × o) (n × o) α) (k : o) : (Matrix.blockDiagAddMonoidHom m n o α) M k = M.blockDiag k

@[simp]

theorem Matrix.blockDiag_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [AddGroup α] (M : Matrix (m × o) (n × o) α) : (-M).blockDiag = -M.blockDiag

@[simp]

theorem Matrix.blockDiag_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [AddGroup α] (M N : Matrix (m × o) (n × o) α) : (M - N).blockDiag = M.blockDiag - N.blockDiag

@[simp]

theorem Matrix.blockDiag_smul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {R : Type u_14} [Monoid R] [AddMonoid α] [DistribMulAction R α] (x : R) (M : Matrix (m × o) (n × o) α) : (x • M).blockDiag = x • M.blockDiag

def Matrix.blockDiagonal' {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [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.

theorem Matrix.blockDiagonal'_apply' {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (k' : o) (j : n' k') : Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', 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} [DecidableEq o] [Zero α] (M : o → Matrix m n α) {k k' : o} (i : m) (j : n) : Matrix.blockDiagonal M (i, k) (j, k') = Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩

theorem Matrix.blockDiagonal'_submatrix_eq_blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : o → Matrix m n α) : (Matrix.blockDiagonal' M).submatrix (Prod.toSigma ∘ Prod.swap) (Prod.toSigma ∘ Prod.swap) = Matrix.blockDiagonal M

theorem Matrix.blockDiagonal'_apply {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (ik : (i : o) × m' i) (jk : (i : o) × n' i) : Matrix.blockDiagonal' M ik jk = 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' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (j : n' k) : Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k, j⟩ = M k i j

theorem Matrix.blockDiagonal'_apply_ne {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) {k k' : o} (i : m' k) (j : n' k') (h : k ≠ k') : Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩ = 0

theorem Matrix.blockDiagonal'_map {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {β : Type u_13} [DecidableEq o] [Zero α] [Zero β] (M : (i : o) → Matrix (m' i) (n' i) α) (f : α → β) (hf : f 0 = 0) : (Matrix.blockDiagonal' M).map f = Matrix.blockDiagonal' fun (k : o) => (M k).map f

@[simp]

theorem Matrix.blockDiagonal'_transpose {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) : (Matrix.blockDiagonal' M).transpose = Matrix.blockDiagonal' fun (k : o) => (M k).transpose

@[simp]

theorem Matrix.blockDiagonal'_conjTranspose {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} [DecidableEq o] {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : (i : o) → Matrix (m' i) (n' i) α) : (Matrix.blockDiagonal' M).conjTranspose = Matrix.blockDiagonal' fun (k : o) => (M k).conjTranspose

@[simp]

theorem Matrix.blockDiagonal'_zero {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [Zero α] : Matrix.blockDiagonal' 0 = 0

@[simp]

theorem Matrix.blockDiagonal'_diagonal {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [DecidableEq o] [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' : o → Type u_7} {α : Type u_12} [DecidableEq o] [Zero α] [(i : o) → DecidableEq (m' i)] [One α] : Matrix.blockDiagonal' 1 = 1

@[simp]

theorem Matrix.blockDiagonal'_add {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [AddZeroClass α] (M N : (i : o) → Matrix (m' i) (n' i) α) : Matrix.blockDiagonal' (M + N) = Matrix.blockDiagonal' M + Matrix.blockDiagonal' N

def Matrix.blockDiagonal'AddMonoidHom {o : Type u_4} (m' : o → Type u_7) (n' : o → Type u_8) (α : Type u_12) [DecidableEq o] [AddZeroClass α] : ((i : o) → Matrix (m' i) (n' i) α) →+ Matrix ((i : o) × m' i) ((i : o) × n' i) α

Matrix.blockDiagonal' as an AddMonoidHom.

Equations

• Matrix.blockDiagonal'AddMonoidHom m' n' α = { toFun := Matrix.blockDiagonal', map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.blockDiagonal'AddMonoidHom_apply {o : Type u_4} (m' : o → Type u_7) (n' : o → Type u_8) (α : Type u_12) [DecidableEq o] [AddZeroClass α] (M : (i : o) → Matrix (m' i) (n' i) α) : (Matrix.blockDiagonal'AddMonoidHom m' n' α) M = Matrix.blockDiagonal' M

@[simp]

theorem Matrix.blockDiagonal'_neg {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [AddGroup α] (M : (i : o) → Matrix (m' i) (n' i) α) : Matrix.blockDiagonal' (-M) = -Matrix.blockDiagonal' M

@[simp]

theorem Matrix.blockDiagonal'_sub {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [AddGroup α] (M N : (i : o) → Matrix (m' i) (n' i) α) : Matrix.blockDiagonal' (M - N) = Matrix.blockDiagonal' M - Matrix.blockDiagonal' N

@[simp]

theorem Matrix.blockDiagonal'_mul {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {p' : o → Type u_9} {α : Type u_12} [DecidableEq o] [NonUnitalNonAssocSemiring α] [(i : o) → Fintype (n' i)] [Fintype o] (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) = Matrix.blockDiagonal' M * Matrix.blockDiagonal' N

def Matrix.blockDiagonal'RingHom {o : Type u_4} (m' : o → Type u_7) (α : Type u_12) [DecidableEq o] [(i : o) → DecidableEq (m' i)] [Fintype o] [(i : o) → Fintype (m' i)] [NonAssocSemiring α] : ((i : o) → Matrix (m' i) (m' i) α) →+* Matrix ((i : o) × m' i) ((i : o) × m' i) α

Matrix.blockDiagonal' as a RingHom.

Equations

• Matrix.blockDiagonal'RingHom m' α = { toFun := Matrix.blockDiagonal', map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.blockDiagonal'RingHom_apply {o : Type u_4} (m' : o → Type u_7) (α : Type u_12) [DecidableEq o] [(i : o) → DecidableEq (m' i)] [Fintype o] [(i : o) → Fintype (m' i)] [NonAssocSemiring α] (M : (i : o) → Matrix (m' i) (m' i) α) : (Matrix.blockDiagonal'RingHom m' α) M = Matrix.blockDiagonal' M

@[simp]

theorem Matrix.blockDiagonal'_pow {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [DecidableEq o] [(i : o) → DecidableEq (m' i)] [Fintype o] [(i : o) → Fintype (m' i)] [Semiring α] (M : (i : o) → Matrix (m' i) (m' i) α) (n : ℕ) : Matrix.blockDiagonal' (M ^ n) = Matrix.blockDiagonal' M ^ n

@[simp]

theorem Matrix.blockDiagonal'_smul {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] {R : Type u_14} [Semiring R] [AddCommMonoid α] [Module R α] (x : R) (M : (i : o) → Matrix (m' i) (n' i) α) : Matrix.blockDiagonal' (x • M) = x • Matrix.blockDiagonal' M

def Matrix.blockDiag' {o : Type u_4} {m' : o → Type u_7} {n' : o → Type 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

• M.blockDiag' k = Matrix.of fun (i : m' k) (j : n' k) => M ⟨k, i⟩ ⟨k, j⟩

theorem Matrix.blockDiag'_apply {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) (i : m' k) (j : n' k) : M.blockDiag' k i j = M ⟨k, i⟩ ⟨k, j⟩

theorem Matrix.blockDiag'_map {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {β : Type u_13} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (f : α → β) : (M.map f).blockDiag' = fun (k : o) => (M.blockDiag' k).map f

@[simp]

theorem Matrix.blockDiag'_transpose {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) : M.transpose.blockDiag' k = (M.blockDiag' k).transpose

@[simp]

theorem Matrix.blockDiag'_conjTranspose {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) : M.conjTranspose.blockDiag' k = (M.blockDiag' k).conjTranspose

@[simp]

theorem Matrix.blockDiag'_zero {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [Zero α] : Matrix.blockDiag' 0 = 0

@[simp]

theorem Matrix.blockDiag'_diagonal {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [Zero α] [DecidableEq o] [(i : o) → DecidableEq (m' i)] (d : (i : o) × m' i → α) (k : o) : (Matrix.diagonal d).blockDiag' k = Matrix.diagonal fun (i : m' k) => d ⟨k, i⟩

@[simp]

theorem Matrix.blockDiag'_blockDiagonal' {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [Zero α] [DecidableEq o] (M : (i : o) → Matrix (m' i) (n' i) α) : (Matrix.blockDiagonal' M).blockDiag' = M

theorem Matrix.blockDiagonal'_injective {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [Zero α] [DecidableEq o] : Function.Injective Matrix.blockDiagonal'

@[simp]

theorem Matrix.blockDiagonal'_inj {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [Zero α] [DecidableEq o] {M N : (i : o) → Matrix (m' i) (n' i) α} : Matrix.blockDiagonal' M = Matrix.blockDiagonal' N ↔ M = N

@[simp]

theorem Matrix.blockDiag'_one {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [Zero α] [DecidableEq o] [(i : o) → DecidableEq (m' i)] [One α] : Matrix.blockDiag' 1 = 1

@[simp]

theorem Matrix.blockDiag'_add {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [AddZeroClass α] (M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : (M + N).blockDiag' = M.blockDiag' + N.blockDiag'

def Matrix.blockDiag'AddMonoidHom {o : Type u_4} (m' : o → Type u_7) (n' : o → Type u_8) (α : Type u_12) [AddZeroClass α] : Matrix ((i : o) × m' i) ((i : o) × n' i) α →+ (i : o) → Matrix (m' i) (n' i) α

Matrix.blockDiag' as an AddMonoidHom.

Equations

• Matrix.blockDiag'AddMonoidHom m' n' α = { toFun := Matrix.blockDiag', map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.blockDiag'AddMonoidHom_apply {o : Type u_4} (m' : o → Type u_7) (n' : o → Type u_8) (α : Type u_12) [AddZeroClass α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) : (Matrix.blockDiag'AddMonoidHom m' n' α) M k = M.blockDiag' k

@[simp]

theorem Matrix.blockDiag'_neg {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [AddGroup α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : (-M).blockDiag' = -M.blockDiag'

@[simp]

theorem Matrix.blockDiag'_sub {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [AddGroup α] (M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : (M - N).blockDiag' = M.blockDiag' - N.blockDiag'

@[simp]

theorem Matrix.blockDiag'_smul {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {R : Type u_14} [Monoid R] [AddMonoid α] [DistribMulAction R α] (x : R) (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : (x • M).blockDiag' = x • M.blockDiag'

theorem Matrix.toBlock_mul_eq_mul {R : Type u_10} [CommRing R] {m : Type u_14} {n : Type u_15} {k : Type u_16} [Fintype n] (p : m → Prop) (q : k → Prop) (A : Matrix m n R) (B : Matrix n k R) : (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q

theorem Matrix.toBlock_mul_eq_add {R : Type u_10} [CommRing R] {m : Type u_14} {n : Type u_15} {k : Type u_16} [Fintype n] (p : m → Prop) (q : n → Prop) [DecidablePred q] (r : k → Prop) (A : Matrix m n R) (B : Matrix n k R) : (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun (i : n) => ¬q i) * B.toBlock (fun (i : n) => ¬q i) r

theorem Matrix.map_toSquareBlock {m : Type u_2} {α : Type u_15} {β : Type u_16} (f : α → β) {M : Matrix m m α} {ι : Type u_18} {b : m → ι} {i : ι} : (M.map f).toSquareBlock b i = (M.toSquareBlock b i).map f

theorem Matrix.comp_toSquareBlock {m : Type u_2} {n : Type u_3} {R : Type u_14} {α : Type u_15} {b : m → α} (M : Matrix m m (Matrix n n R)) (a : α) : ((Matrix.comp m m n n R) M).toSquareBlock (fun (i : m × n) => b i.1) a = (Matrix.reindex Equiv.prodSubtypeFstEquivSubtypeProd.symm Equiv.prodSubtypeFstEquivSubtypeProd.symm) ((Matrix.comp { a_1 : m // b a_1 = a } { a_1 : m // b a_1 = a } n n R) (M.toSquareBlock b a))

theorem Matrix.comp_diagonal {m : Type u_2} {n : Type u_3} {R : Type u_14} [Zero R] [DecidableEq m] (d : m → Matrix n n R) : (Matrix.comp m m n n R) (Matrix.diagonal d) = (Matrix.reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (Matrix.blockDiagonal d)