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.

@[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) : 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) : 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) : 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) : 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) α) : 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 α) : (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 α) : (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 α) : (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 α) : (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 α} : fromBlocks A B C D = 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 : α → β) : (fromBlocks A B C D).map f = 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 α) : (fromBlocks A B C D).transpose = 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 α) : (fromBlocks A B C D).conjTranspose = 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) : (fromBlocks A B C D).submatrix Sum.swap f = (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) : (fromBlocks A B C D).submatrix f Sum.swap = (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 α) : (fromBlocks A B C D).submatrix Sum.swap Sum.swap = 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 : 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.

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

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

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 = 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 • fromBlocks A B C D = 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) : -fromBlocks A B C D = 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 α] : 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 α) : fromBlocks A B C D + fromBlocks A' B' C' D' = 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 α) : fromBlocks A B C D * fromBlocks A' B' C' D' = fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

theorem Matrix.fromBlocks_diagonal_pow {m : Type u_2} {n : Type u_3} {α : Type u_12} [Semiring α] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (A : Matrix n n α) (D : Matrix m m α) (k : ℕ) : fromBlocks A 0 0 D ^ k = fromBlocks (A ^ k) 0 0 (D ^ k)

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 → α) : (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 → α) : vecMul x (fromBlocks A B C D) = Sum.elim (vecMul (x ∘ Sum.inl) A + vecMul (x ∘ Sum.inr) C) (vecMul (x ∘ Sum.inl) B + 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) : (diagonal d).toBlock p p = 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) : (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 → α) : fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = 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 → α) : (diagonal v).toBlocks₁₁ = 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 → α) : (diagonal v).toBlocks₂₂ = 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 → α) : (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 → α) : (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 α] : 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) : 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) : 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 homogeneously-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) : 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) : 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) : 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') : 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) : (blockDiagonal M).map f = 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 α) : (blockDiagonal M).transpose = 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 α) : (blockDiagonal M).conjTranspose = 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 α] : 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 → α) : (blockDiagonal fun (k : o) => diagonal (d k)) = 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 α] : 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 α) : blockDiagonal (M + N) = blockDiagonal M + 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.

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

@[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 α) : (blockDiagonalRingHom m o α) M = 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 : ℕ) : blockDiagonal (M ^ n) = 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} [Zero α] [SMulZeroClass R α] (x : R) (M : o → Matrix m n α) : blockDiagonal (x • M) = x • 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) : 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} [Star α] (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 α] : 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) : (diagonal d).blockDiag k = 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 α) : (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 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 α} : blockDiagonal M = 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 α] : blockDiag 1 = 1

@[simp]

theorem Matrix.blockDiag_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Add α] (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.

@[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) : (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} [SMul 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.

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') : 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) : blockDiagonal M (i, k) (j, k') = 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 α) : (blockDiagonal' M).submatrix (Prod.toSigma ∘ Prod.swap) (Prod.toSigma ∘ Prod.swap) = 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) : 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) : 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') : 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) : (blockDiagonal' M).map f = 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) α) : (blockDiagonal' M).transpose = 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) α) : (blockDiagonal' M).conjTranspose = 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 α] : 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 → α) : (blockDiagonal' fun (k : o) => diagonal (d k)) = 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 α] : 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) α) : blockDiagonal' (M + N) = blockDiagonal' M + 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.

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

@[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) α) : (blockDiagonal'RingHom m' α) M = 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 : ℕ) : blockDiagonal' (M ^ n) = 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} [Zero α] [SMulZeroClass R α] (x : R) (M : (i : o) → Matrix (m' i) (n' i) α) : blockDiagonal' (x • M) = x • 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) : 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} [Star α] (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 α] : 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) : (diagonal d).blockDiag' k = 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) α) : (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 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) α} : blockDiagonal' M = 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 α] : 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} [Add α] (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.

@[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) : (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} [SMul 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 : α) : ((comp m m n n R) M).toSquareBlock (fun (i : m × n) => b i.1) a = (reindex Equiv.prodSubtypeFstEquivSubtypeProd.symm Equiv.prodSubtypeFstEquivSubtypeProd.symm) ((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) : (comp m m n n R) (diagonal d) = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d)