Block Matrices #
Main definitions #
matrix.from_blocks: build a block matrix out of 4 blocksmatrix.to_blocks₁₁,matrix.to_blocks₁₂,matrix.to_blocks₂₁,matrix.to_blocks₂₂: extract each of the four blocks frommatrix.from_blocks.matrix.block_diagonal: block diagonal of equally sized blocks. On square blocks, this is a ring homomorphisms,matrix.block_diagonal_ring_hom.matrix.block_diagonal': block diagonal of unequally sized blocks. On square blocks, this is a ring homomorphisms,matrix.block_diagonal'_ring_hom.
def
matrix.from_blocks
{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 α) :
We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.
Equations
- matrix.from_blocks A B C D = sum.elim (λ (i : n), sum.elim (A i) (B i)) (λ (i : o), sum.elim (C i) (D i))
@[simp]
theorem
matrix.from_blocks_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.from_blocks A B C D (sum.inl i) (sum.inl j) = A i j
@[simp]
theorem
matrix.from_blocks_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.from_blocks A B C D (sum.inl i) (sum.inr j) = B i j
@[simp]
theorem
matrix.from_blocks_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.from_blocks A B C D (sum.inr i) (sum.inl j) = C i j
@[simp]
theorem
matrix.from_blocks_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.from_blocks A B C D (sum.inr i) (sum.inr j) = D i j
def
matrix.to_blocks₁₁
{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.to_blocks₁₁ = λ (i : n) (j : l), M (sum.inl i) (sum.inl j)
def
matrix.to_blocks₁₂
{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.to_blocks₁₂ = λ (i : n) (j : m), M (sum.inl i) (sum.inr j)
def
matrix.to_blocks₂₁
{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.to_blocks₂₁ = λ (i : o) (j : l), M (sum.inr i) (sum.inl j)
def
matrix.to_blocks₂₂
{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.to_blocks₂₂ = λ (i : o) (j : m), M (sum.inr i) (sum.inr j)
theorem
matrix.from_blocks_to_blocks
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
@[simp]
theorem
matrix.to_blocks_from_blocks₁₁
{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.from_blocks A B C D).to_blocks₁₁ = A
@[simp]
theorem
matrix.to_blocks_from_blocks₁₂
{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.from_blocks A B C D).to_blocks₁₂ = B
@[simp]
theorem
matrix.to_blocks_from_blocks₂₁
{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.from_blocks A B C D).to_blocks₂₁ = C
@[simp]
theorem
matrix.to_blocks_from_blocks₂₂
{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.from_blocks A B C D).to_blocks₂₂ = D
theorem
matrix.from_blocks_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.from_blocks A B C D).map f = matrix.from_blocks (A.map f) (B.map f) (C.map f) (D.map f)
theorem
matrix.from_blocks_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.from_blocks A B C D)ᵀ = matrix.from_blocks Aᵀ Cᵀ Bᵀ Dᵀ
theorem
matrix.from_blocks_conj_transpose
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[has_star α]
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(matrix.from_blocks A B C D)ᴴ = matrix.from_blocks Aᴴ Cᴴ Bᴴ Dᴴ
def
matrix.is_two_block_diagonal
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[has_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.is_two_block_diagonal = (A.to_blocks₁₂ = 0 ∧ A.to_blocks₂₁ = 0)
def
matrix.to_block
{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
to_block M p q is the corresponding block matrix.
def
matrix.to_square_block
{m : Type u_2}
{α : Type u_12}
(M : matrix m m α)
{n : ℕ}
(b : m → fin n)
(k : fin n) :
Let b map rows and columns of a square matrix M to blocks. Then
to_square_block M b k is the block k matrix.
Equations
- M.to_square_block b k = M.minor coe coe
Alternate version with b : m → nat. Let b map rows and columns of a square matrix M to
blocks. Then to_square_block' M b k is the block k matrix.
Equations
- M.to_square_block' b k = M.minor coe coe
@[simp]
theorem
matrix.to_square_block_def'
{m : Type u_2}
{α : Type u_12}
(M : matrix m m α)
(b : m → ℕ)
(k : ℕ) :
M.to_square_block' b k = λ (i j : {a // b a = k}), M ↑i ↑j
def
matrix.to_square_block_prop
{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
to_square_block_prop M p is the corresponding block matrix.
Equations
- M.to_square_block_prop p = M.minor coe coe
@[simp]
theorem
matrix.to_square_block_prop_def
{m : Type u_2}
{α : Type u_12}
(M : matrix m m α)
(p : m → Prop) :
M.to_square_block_prop p = λ (i j : {a // p a}), M ↑i ↑j
theorem
matrix.from_blocks_smul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{R : Type u_10}
{α : Type u_12}
[has_scalar R α]
(x : R)
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
x • matrix.from_blocks A B C D = matrix.from_blocks (x • A) (x • B) (x • C) (x • D)
theorem
matrix.from_blocks_add
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[has_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.from_blocks A B C D + matrix.from_blocks A' B' C' D' = matrix.from_blocks (A + A') (B + B') (C + C') (D + D')
theorem
matrix.from_blocks_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]
[non_unital_non_assoc_semiring α]
(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 α) :
@[simp]
theorem
matrix.from_blocks_diagonal
{l : Type u_1}
{m : Type u_2}
{α : Type u_12}
[decidable_eq l]
[decidable_eq m]
[has_zero α]
(d₁ : l → α)
(d₂ : m → α) :
matrix.from_blocks (matrix.diagonal d₁) 0 0 (matrix.diagonal d₂) = matrix.diagonal (sum.elim d₁ d₂)
@[simp]
theorem
matrix.from_blocks_one
{l : Type u_1}
{m : Type u_2}
{α : Type u_12}
[decidable_eq l]
[decidable_eq m]
[has_zero α]
[has_one α] :
matrix.from_blocks 1 0 0 1 = 1
def
matrix.block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α) :
matrix.block_diagonal M turns a homogenously-indexed collection of matrices
M : o → matrix m n α' into a m × o-by-n × o block matrix which has the entries of M along
the diagonal and zero elsewhere.
See also matrix.block_diagonal' if the matrices may not have the same size everywhere.
Equations
- matrix.block_diagonal M (i, k) (j, k') = ite (k = k') (M k i j) 0
@[simp]
theorem
matrix.block_diagonal_apply_eq
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α)
(i : m)
(j : n)
(k : o) :
matrix.block_diagonal M (i, k) (j, k) = M k i j
theorem
matrix.block_diagonal_apply_ne
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α)
(i : m)
(j : n)
{k k' : o}
(h : k ≠ k') :
matrix.block_diagonal M (i, k) (j, k') = 0
theorem
matrix.block_diagonal_map
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
{β : Type u_13}
[decidable_eq o]
[has_zero α]
[has_zero β]
(M : o → matrix m n α)
(f : α → β)
(hf : f 0 = 0) :
(matrix.block_diagonal M).map f = matrix.block_diagonal (λ (k : o), (M k).map f)
@[simp]
theorem
matrix.block_diagonal_transpose
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α) :
(matrix.block_diagonal M)ᵀ = matrix.block_diagonal (λ (k : o), (M k)ᵀ)
@[simp]
theorem
matrix.block_diagonal_conj_transpose
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[decidable_eq o]
{α : Type u_1}
[add_monoid α]
[star_add_monoid α]
(M : o → matrix m n α) :
(matrix.block_diagonal M)ᴴ = matrix.block_diagonal (λ (k : o), (M k)ᴴ)
@[simp]
theorem
matrix.block_diagonal_zero
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α] :
@[simp]
theorem
matrix.block_diagonal_diagonal
{m : Type u_2}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[decidable_eq m]
(d : o → m → α) :
matrix.block_diagonal (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : m × o), d ik.snd ik.fst)
@[simp]
theorem
matrix.block_diagonal_one
{m : Type u_2}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[decidable_eq m]
[has_one α] :
@[simp]
theorem
matrix.block_diagonal_add
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[add_zero_class α]
(M N : o → matrix m n α) :
@[simp]
theorem
matrix.block_diagonal_add_monoid_hom_apply
(m : Type u_2)
(n : Type u_3)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α]
(M : o → matrix m n α) :
⇑(matrix.block_diagonal_add_monoid_hom m n o α) M = matrix.block_diagonal M
def
matrix.block_diagonal_add_monoid_hom
(m : Type u_2)
(n : Type u_3)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α] :
matrix.block_diagonal as an add_monoid_hom.
Equations
- matrix.block_diagonal_add_monoid_hom m n o α = {to_fun := matrix.block_diagonal (add_zero_class.to_has_zero α), map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal_neg
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M : o → matrix m n α) :
@[simp]
theorem
matrix.block_diagonal_sub
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M N : o → matrix m n α) :
@[simp]
theorem
matrix.block_diagonal_mul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{p : Type u_5}
{α : Type u_12}
[decidable_eq o]
[fintype n]
[fintype o]
[non_unital_non_assoc_semiring α]
(M : o → matrix m n α)
(N : o → matrix n p α) :
matrix.block_diagonal (λ (k : o), M k ⬝ N k) = matrix.block_diagonal M ⬝ matrix.block_diagonal N
@[simp]
theorem
matrix.block_diagonal_ring_hom_apply
(m : Type u_2)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[decidable_eq m]
[fintype o]
[fintype m]
[non_assoc_semiring α]
(M : o → matrix m m α) :
⇑(matrix.block_diagonal_ring_hom m o α) M = matrix.block_diagonal M
def
matrix.block_diagonal_ring_hom
(m : Type u_2)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[decidable_eq m]
[fintype o]
[fintype m]
[non_assoc_semiring α] :
matrix.block_diagonal as a ring_hom.
Equations
- matrix.block_diagonal_ring_hom m o α = {to_fun := matrix.block_diagonal (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal_smul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
{R : Type u_1}
[monoid R]
[add_monoid α]
[distrib_mul_action R α]
(x : R)
(M : o → matrix m n α) :
matrix.block_diagonal (x • M) = x • matrix.block_diagonal M
def
matrix.block_diagonal'
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α
matrix.block_diagonal' 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.block_diagonal.
theorem
matrix.block_diagonal'_eq_block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α)
{k k' : o}
(i : m)
(j : n) :
matrix.block_diagonal M (i, k) (j, k') = matrix.block_diagonal' M ⟨k, i⟩ ⟨k', j⟩
theorem
matrix.block_diagonal'_minor_eq_block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α) :
theorem
matrix.block_diagonal'_apply
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α)
(ik : Σ (i : o), m' i)
(jk : Σ (i : o), n' i) :
@[simp]
theorem
matrix.block_diagonal'_apply_eq
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α)
(k : o)
(i : m' k)
(j : n' k) :
matrix.block_diagonal' M ⟨k, i⟩ ⟨k, j⟩ = M k i j
theorem
matrix.block_diagonal'_apply_ne
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α)
{k k' : o}
(i : m' k)
(j : n' k')
(h : k ≠ k') :
matrix.block_diagonal' M ⟨k, i⟩ ⟨k', j⟩ = 0
theorem
matrix.block_diagonal'_map
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
{β : Type u_13}
[decidable_eq o]
[has_zero α]
[has_zero β]
(M : Π (i : o), matrix (m' i) (n' i) α)
(f : α → β)
(hf : f 0 = 0) :
(matrix.block_diagonal' M).map f = matrix.block_diagonal' (λ (k : o), (M k).map f)
@[simp]
theorem
matrix.block_diagonal'_transpose
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
(matrix.block_diagonal' M)ᵀ = matrix.block_diagonal' (λ (k : o), (M k)ᵀ)
@[simp]
theorem
matrix.block_diagonal'_conj_transpose
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
[decidable_eq o]
{α : Type u_1}
[add_monoid α]
[star_add_monoid α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
(matrix.block_diagonal' M)ᴴ = matrix.block_diagonal' (λ (k : o), (M k)ᴴ)
@[simp]
theorem
matrix.block_diagonal'_zero
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α] :
@[simp]
theorem
matrix.block_diagonal'_diagonal
{o : Type u_4}
{m' : o → Type u_7}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[Π (i : o), decidable_eq (m' i)]
(d : Π (i : o), m' i → α) :
matrix.block_diagonal' (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : Σ (i : o), m' i), d ik.fst ik.snd)
@[simp]
theorem
matrix.block_diagonal'_one
{o : Type u_4}
{m' : o → Type u_7}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[Π (i : o), decidable_eq (m' i)]
[has_one α] :
@[simp]
theorem
matrix.block_diagonal'_add
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[add_zero_class α]
(M N : Π (i : o), matrix (m' i) (n' i) α) :
def
matrix.block_diagonal'_add_monoid_hom
{o : Type u_4}
(m' : o → Type u_7)
(n' : o → Type u_8)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α] :
matrix.block_diagonal' as an add_monoid_hom.
Equations
- matrix.block_diagonal'_add_monoid_hom m' n' α = {to_fun := matrix.block_diagonal' (add_zero_class.to_has_zero α), map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal'_add_monoid_hom_apply
{o : Type u_4}
(m' : o → Type u_7)
(n' : o → Type u_8)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α]
(M : Π (i : o), matrix ((λ (i : o), m' i) i) ((λ (i : o), n' i) i) α) :
⇑(matrix.block_diagonal'_add_monoid_hom m' n' α) M = matrix.block_diagonal' M
@[simp]
theorem
matrix.block_diagonal'_neg
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
@[simp]
theorem
matrix.block_diagonal'_sub
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M N : Π (i : o), matrix (m' i) (n' i) α) :
@[simp]
theorem
matrix.block_diagonal'_mul
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{p' : o → Type u_9}
{α : Type u_12}
[decidable_eq o]
[non_unital_non_assoc_semiring α]
[Π (i : o), fintype (n' i)]
[fintype o]
(M : Π (i : o), matrix (m' i) (n' i) α)
(N : Π (i : o), matrix (n' i) (p' i) α) :
matrix.block_diagonal' (λ (k : o), M k ⬝ N k) = matrix.block_diagonal' M ⬝ matrix.block_diagonal' N
def
matrix.block_diagonal'_ring_hom
{o : Type u_4}
(m' : o → Type u_7)
(α : Type u_12)
[decidable_eq o]
[Π (i : o), decidable_eq (m' i)]
[fintype o]
[Π (i : o), fintype (m' i)]
[non_assoc_semiring α] :
matrix.block_diagonal' as a ring_hom.
Equations
- matrix.block_diagonal'_ring_hom m' α = {to_fun := matrix.block_diagonal' (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal'_ring_hom_apply
{o : Type u_4}
(m' : o → Type u_7)
(α : Type u_12)
[decidable_eq o]
[Π (i : o), decidable_eq (m' i)]
[fintype o]
[Π (i : o), fintype (m' i)]
[non_assoc_semiring α]
(M : Π (i : o), matrix ((λ (i : o), m' i) i) ((λ (i : o), m' i) i) α) :
@[simp]
theorem
matrix.block_diagonal'_smul
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
{R : Type u_1}
[semiring R]
[add_comm_monoid α]
[module R α]
(x : R)
(M : Π (i : o), matrix (m' i) (n' i) α) :
matrix.block_diagonal' (x • M) = x • matrix.block_diagonal' M