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 : m ⊕ n → α) (w : m ⊕ n → α) : Matrix.dotProduct v w = 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.

@[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.

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.

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.

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.

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 (Matrix.toBlocks₁₁ M) (Matrix.toBlocks₁₂ M) (Matrix.toBlocks₂₁ M) (Matrix.toBlocks₂₂ M) = 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.toBlocks₁₁ (Matrix.fromBlocks A B C D) = 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.toBlocks₁₂ (Matrix.fromBlocks A B C D) = 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.toBlocks₂₁ (Matrix.fromBlocks A B C D) = 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.toBlocks₂₂ (Matrix.fromBlocks A B C D) = 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 : Matrix (n ⊕ o) (l ⊕ m) α} {B : Matrix (n ⊕ o) (l ⊕ m) α} : A = B ↔ Matrix.toBlocks₁₁ A = Matrix.toBlocks₁₁ B ∧ Matrix.toBlocks₁₂ A = Matrix.toBlocks₁₂ B ∧ Matrix.toBlocks₂₁ A = Matrix.toBlocks₂₁ B ∧ Matrix.toBlocks₂₂ A = Matrix.toBlocks₂₂ 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 = 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 (Matrix.fromBlocks A B C D) f = Matrix.fromBlocks (Matrix.map A f) (Matrix.map B f) (Matrix.map C f) (Matrix.map D 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.transpose (Matrix.fromBlocks A B C D) = Matrix.fromBlocks (Matrix.transpose A) (Matrix.transpose C) (Matrix.transpose B) (Matrix.transpose D)

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

@[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.submatrix (Matrix.fromBlocks A B C D) Sum.swap f = Matrix.submatrix (Matrix.fromBlocks C D A B) 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.submatrix (Matrix.fromBlocks A B C D) f Sum.swap = Matrix.submatrix (Matrix.fromBlocks B A D C) 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 (Matrix.fromBlocks A B C D) 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

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 // p a } { a // 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.

@[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 // p a }) (j : { a // 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 : m → Prop) : Matrix { a // p a } { a // p a } α

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

theorem Matrix.toSquareBlockProp_def {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : m → Prop) : Matrix.toSquareBlockProp M p = ↑Matrix.of fun i j => 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 // b a = k } { a // 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.

theorem Matrix.toSquareBlock_def {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : Matrix m m α) (b : m → β) (k : β) : Matrix.toSquareBlock M b k = ↑Matrix.of fun i j => 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.mulVec (Matrix.fromBlocks A B C D) 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} [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.toBlock (Matrix.diagonal d) p p = Matrix.diagonal fun i => d ↑i

theorem Matrix.toBlock_diagonal_disjoint {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] (d : m → α) {p : m → Prop} {q : m → Prop} (hpq : Disjoint p q) : Matrix.toBlock (Matrix.diagonal d) 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.toBlocks₁₁ (Matrix.diagonal v) = Matrix.diagonal fun i => 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.toBlocks₂₂ (Matrix.diagonal v) = Matrix.diagonal fun i => 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.toBlocks₁₂ (Matrix.diagonal v) = 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.toBlocks₂₁ (Matrix.diagonal v) = 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 : m → Prop} {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.

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.snd = jk.snd then M ik.snd ik.fst jk.fst 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 : 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} [DecidableEq o] [Zero α] [Zero β] (M : o → Matrix m n α) (f : α → β) (hf : f 0 = 0) : Matrix.map (Matrix.blockDiagonal M) f = Matrix.blockDiagonal fun k => 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} [DecidableEq o] [Zero α] (M : o → Matrix m n α) : Matrix.transpose (Matrix.blockDiagonal M) = Matrix.blockDiagonal fun k => Matrix.transpose (M k)

@[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.conjTranspose (Matrix.blockDiagonal M) = Matrix.blockDiagonal fun k => Matrix.conjTranspose (M k)

@[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 => Matrix.diagonal (d k)) = Matrix.diagonal fun ik => d ik.snd ik.fst

@[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 : o → Matrix m n α) (N : o → Matrix m n α) : Matrix.blockDiagonal (M + N) = Matrix.blockDiagonal M + Matrix.blockDiagonal N

@[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

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.

@[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 : o → Matrix m n α) (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 => M k * N k) = Matrix.blockDiagonal M * Matrix.blockDiagonal N

@[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

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.

@[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.

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

@[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) : Matrix.blockDiag (Matrix.conjTranspose M) k = Matrix.conjTranspose (Matrix.blockDiag M k)

@[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.blockDiag (Matrix.diagonal d) k = Matrix.diagonal fun i => 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.blockDiag (Matrix.blockDiagonal M) = 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 : o → Matrix m n α} {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 : Matrix (m × o) (n × o) α) (N : Matrix (m × o) (n × o) α) : Matrix.blockDiag (M + N) = Matrix.blockDiag M + Matrix.blockDiag N

@[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 = Matrix.blockDiag M k

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.

@[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) α) : Matrix.blockDiag (-M) = -Matrix.blockDiag M

@[simp]

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

@[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) α) : Matrix.blockDiag (x • M) = x • Matrix.blockDiag M

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.

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 { fst := k, snd := i } { fst := k', snd := j } = if h : k = k' then M k i (cast (_ : n' k' = n' k) 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 : 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} [DecidableEq o] [Zero α] (M : o → Matrix m n α) : Matrix.submatrix (Matrix.blockDiagonal' M) (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 (_ : n' jk.fst = n' ik.fst) 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 { fst := k, snd := i } { fst := k, snd := 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 : 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' : 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.map (Matrix.blockDiagonal' M) f = Matrix.blockDiagonal' fun k => Matrix.map (M k) 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.transpose (Matrix.blockDiagonal' M) = Matrix.blockDiagonal' fun k => Matrix.transpose (M k)

@[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.conjTranspose (Matrix.blockDiagonal' M) = Matrix.blockDiagonal' fun k => Matrix.conjTranspose (M k)

@[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 => Matrix.diagonal (d k)) = Matrix.diagonal fun ik => 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 : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (m' i) (n' i) α) : Matrix.blockDiagonal' (M + N) = Matrix.blockDiagonal' M + Matrix.blockDiagonal' N

@[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

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.

@[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 : (i : o) → Matrix (m' i) (n' i) α) (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 => M k * N k) = Matrix.blockDiagonal' M * Matrix.blockDiagonal' N

@[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

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.

@[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'.

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) : Matrix.blockDiag' M k i j = M { fst := k, snd := i } { fst := k, snd := 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 : α → β) : Matrix.blockDiag' (Matrix.map M f) = fun k => Matrix.map (Matrix.blockDiag' M k) 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) : Matrix.blockDiag' (Matrix.transpose M) k = Matrix.transpose (Matrix.blockDiag' M k)

@[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) : Matrix.blockDiag' (Matrix.conjTranspose M) k = Matrix.conjTranspose (Matrix.blockDiag' M k)

@[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.blockDiag' (Matrix.diagonal d) k = Matrix.diagonal fun i => d { fst := k, snd := 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.blockDiag' (Matrix.blockDiagonal' M) = 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 : (i : o) → Matrix (m' i) (n' i) α} {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 : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : Matrix.blockDiag' (M + N) = Matrix.blockDiag' M + Matrix.blockDiag' N

@[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 = Matrix.blockDiag' M k

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.

@[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) α) : Matrix.blockDiag' (-M) = -Matrix.blockDiag' M

@[simp]

theorem Matrix.blockDiag'_sub {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) α) (N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : Matrix.blockDiag' (M - N) = Matrix.blockDiag' M - Matrix.blockDiag' N

@[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) α) : Matrix.blockDiag' (x • M) = x • Matrix.blockDiag' M

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) : Matrix.toBlock (A * B) p q = Matrix.toBlock A p ⊤ * Matrix.toBlock B ⊤ 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) : Matrix.toBlock (A * B) p r = Matrix.toBlock A p q * Matrix.toBlock B q r + (Matrix.toBlock A p fun i => ¬q i) * Matrix.toBlock B (fun i => ¬q i) r