Include block #
This file defines matrix.include_block which immitates direct_sum.component_of but for pi instead of direct_sum :TODO:
The direct sum in these files are sort of misleading.
theorem
finset.sum_sigma_univ
{β : Type u_1}
{α : Type u_2}
[add_comm_monoid β]
[fintype α]
{σ : α → Type u_3}
[Π (i : α), fintype (σ i)]
(f : (Σ (i : α), σ i) → β) :
finset.univ.sum (λ (x : Σ (i : α), σ i), f x) = finset.univ.sum (λ (a : α), finset.univ.sum (λ (s : σ a), f ⟨a, s⟩))
def
matrix.block_diagonal'_alg_hom
{o : Type u_1}
{m' : o → Type u_2}
{α : Type u_3}
[fintype o]
[decidable_eq o]
[Π (i : o), fintype (m' i)]
[Π (i : o), decidable_eq (m' i)]
[comm_semiring α] :
theorem
matrix.block_diagonal'_alg_hom_apply
{o : Type u_1}
{m' : o → Type u_2}
{α : Type u_3}
[fintype o]
[decidable_eq o]
[Π (i : o), fintype (m' i)]
[Π (i : o), decidable_eq (m' i)]
[comm_semiring α]
(x : Π (i : o), matrix (m' i) (m' i) α) :
theorem
matrix.block_diag'_linear_map_block_diagonal'_alg_hom
{o : Type u_1}
{m' : o → Type u_2}
{α : Type u_3}
[fintype o]
[decidable_eq o]
[Π (i : o), fintype (m' i)]
[Π (i : o), decidable_eq (m' i)]
[comm_semiring α]
(x : Π (i : o), matrix (m' i) (m' i) α) :
def
matrix.include_block
{o : Type u_1}
[decidable_eq o]
{m' : o → Type u_2}
{α : Type u_3}
[comm_semiring α]
{i : o} :
Equations
theorem
matrix.include_block_apply
{o : Type u_1}
[decidable_eq o]
{m' : o → Type u_2}
{α : Type u_3}
[comm_semiring α]
{i : o}
(x : matrix (m' i) (m' i) α) :
theorem
matrix.include_block_mul_same
{o : Type u_1}
[fintype o]
[decidable_eq o]
{m' : o → Type u_2}
{α : Type u_3}
[Π (i : o), fintype (m' i)]
[Π (i : o), decidable_eq (m' i)]
[comm_semiring α]
{i : o}
(x y : matrix (m' i) (m' i) α) :
theorem
matrix.include_block_mul_ne_same
{o : Type u_1}
[fintype o]
[decidable_eq o]
{m' : o → Type u_2}
{α : Type u_3}
[Π (i : o), fintype (m' i)]
[Π (i : o), decidable_eq (m' i)]
[comm_semiring α]
{i j : o}
(h : i ≠ j)
(x : matrix (m' i) (m' i) α)
(y : matrix (m' j) (m' j) α) :
theorem
matrix.include_block_mul
{o : Type u_1}
[fintype o]
[decidable_eq o]
{m' : o → Type u_2}
{α : Type u_3}
[Π (i : o), fintype (m' i)]
[Π (i : o), decidable_eq (m' i)]
[comm_semiring α]
{i : o}
(x : matrix (m' i) (m' i) α)
(y : Π (j : o), matrix (m' j) (m' j) α) :
⇑matrix.include_block x * y = ⇑matrix.include_block (x * y i)
theorem
matrix.mul_include_block
{o : Type u_1}
[fintype o]
[decidable_eq o]
{m' : o → Type u_2}
{α : Type u_3}
[Π (i : o), fintype (m' i)]
[Π (i : o), decidable_eq (m' i)]
[comm_semiring α]
{i : o}
(x : Π (j : o), matrix (m' j) (m' j) α)
(y : matrix (m' i) (m' i) α) :
x * ⇑matrix.include_block y = ⇑matrix.include_block (x i * y)
theorem
matrix.sum_include_block
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : Π (i : k), matrix (s i) (s i) R) :
finset.univ.sum (λ (i : k), ⇑matrix.include_block (x i)) = x
theorem
matrix.block_diagonal'_include_block_trace
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : Π (i : k), matrix (s i) (s i) R)
(j : k) :
(matrix.block_diagonal' (⇑matrix.include_block (x j))).trace = (x j).trace
theorem
matrix.std_basis_matrix_mul_trace
{R : Type u_1}
{n : Type u_2}
{p : Type u_3}
[semiring R]
[fintype p]
[decidable_eq p]
[fintype n]
[decidable_eq n]
(i : n)
(j : p)
(x : matrix p n R) :
((matrix.std_basis_matrix i j 1).mul x).trace = x j i
theorem
matrix.ext_iff_trace
{R : Type u_1}
{n : Type u_2}
{p : Type u_3}
[fintype n]
[fintype p]
[decidable_eq n]
[decidable_eq p]
[comm_semiring R]
(x y : matrix n p R) :
theorem
matrix.is_block_diagonal.eq
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
{x : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal) :
theorem
matrix.is_block_diagonal.add
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
{x y : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal)
(hy : y.is_block_diagonal) :
(x + y).is_block_diagonal
theorem
matrix.is_block_diagonal.zero
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3} :
@[protected, instance]
def
matrix.add_comm_monoid_block_diagonal
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
add_comm_monoid {x // x.is_block_diagonal}
Equations
- matrix.add_comm_monoid_block_diagonal = {add := λ (x y : {x // x.is_block_diagonal}), ⟨↑x + ↑y, _⟩, add_assoc := _, zero := ⟨0, _⟩, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default ⟨0, _⟩ (λ (x y : {x // x.is_block_diagonal}), ⟨↑x + ↑y, _⟩) matrix.add_comm_monoid_block_diagonal._proof_6 matrix.add_comm_monoid_block_diagonal._proof_7, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
theorem
matrix.is_block_diagonal.coe_add
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{x y : {x // x.is_block_diagonal}} :
theorem
matrix.is_block_diagonal.coe_sum
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{n : Type u_4}
[fintype n]
{x : n → {x // x.is_block_diagonal}} :
↑(finset.univ.sum (λ (i : n), x i)) = finset.univ.sum (λ (i : n), ↑(x i))
theorem
matrix.is_block_diagonal.coe_zero
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
theorem
matrix.is_block_diagonal.smul
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
{x : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal)
(α : R) :
(α • x).is_block_diagonal
@[protected, instance]
def
matrix.has_smul_block_diagonal
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
has_smul R {x // x.is_block_diagonal}
Equations
- matrix.has_smul_block_diagonal = {smul := λ (a : R) (x : {x // x.is_block_diagonal}), ⟨a • ↑x, _⟩}
theorem
matrix.is_block_diagonal.coe_smul
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(a : R)
(x : {x // x.is_block_diagonal}) :
@[protected, instance]
def
matrix.mul_action_block_diagonal
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
mul_action R {x // x.is_block_diagonal}
Equations
- matrix.mul_action_block_diagonal = {to_has_smul := matrix.has_smul_block_diagonal (λ (i : k) (a b : s i), _inst_5 i a b), one_smul := _, mul_smul := _}
@[protected, instance]
def
matrix.distrib_mul_action_block_diagonal
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
distrib_mul_action R {x // x.is_block_diagonal}
Equations
- matrix.distrib_mul_action_block_diagonal = {to_mul_action := matrix.mul_action_block_diagonal (λ (i : k) (a b : s i), _inst_5 i a b), smul_zero := _, smul_add := _}
@[protected, instance]
def
matrix.module_block_diagonal
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
module R {x // x.is_block_diagonal}
Equations
- matrix.module_block_diagonal = {to_distrib_mul_action := matrix.distrib_mul_action_block_diagonal (λ (i : k) (a b : s i), _inst_5 i a b), add_smul := _, zero_smul := _}
theorem
matrix.is_block_diagonal.block_diagonal'
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
(x : Π (i : k), matrix (s i) (s i) R) :
theorem
matrix.is_block_diagonal_iff
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
(x : matrix (Σ (i : k), s i) (Σ (i : k), s i) R) :
x.is_block_diagonal ↔ ∃ (y : Π (i : k), matrix (s i) (s i) R), x = matrix.block_diagonal' y
def
matrix.std_basis_matrix_block_diagonal
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), decidable_eq (s i)]
(i : k)
(j l : s i)
(α : R) :
{x // x.is_block_diagonal}
Equations
- matrix.std_basis_matrix_block_diagonal i j l α = ⟨matrix.std_basis_matrix ⟨i, j⟩ ⟨i, l⟩ α, _⟩
theorem
matrix.include_block_conj_transpose
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[star_ring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{i : k}
{x : matrix (s i) (s i) R} :
theorem
matrix.include_block_inj
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{i : k}
{x y : matrix (s i) (s i) R} :
⇑matrix.include_block x = ⇑matrix.include_block y ↔ x = y
theorem
matrix.block_diagonal'_include_block_is_hermitian_iff
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[star_ring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{i : k}
(x : matrix (s i) (s i) R) :
theorem
matrix.matrix_eq_sum_include_block
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : Π (i : k), matrix (s i) (s i) R) :
x = finset.univ.sum (λ (i : k), ⇑matrix.include_block (x i))
theorem
matrix.include_block_apply_same
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{i : k}
(x : matrix (s i) (s i) R) :
⇑matrix.include_block x i = x
theorem
matrix.include_block_apply_ne_same
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{i j : k}
(x : matrix (s i) (s i) R)
(h : i ≠ j) :
⇑matrix.include_block x j = 0
theorem
matrix.include_block_apply_std_basis_matrix
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{i : k}
(a b : s i) :
⇑matrix.include_block (matrix.std_basis_matrix a b 1) = (matrix.std_basis_matrix ⟨i, a⟩ ⟨i, b⟩ 1).block_diag'
theorem
matrix.include_block_mul_include_block
{R : Type u_1}
{k : Type u_2}
[comm_semiring R]
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{i j : k}
(x : matrix (s i) (s i) R)
(y : matrix (s j) (s j) R) :
⇑matrix.include_block x * ⇑matrix.include_block y = dite (j = i) (λ (h : j = i), ⇑matrix.include_block (x * _.mpr y)) (λ (h : ¬j = i), 0)
theorem
matrix.is_block_diagonal.mul
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
{x y : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal)
(hy : y.is_block_diagonal) :
(x.mul y).is_block_diagonal
@[instance]
def
matrix.is_block_diagonal.has_mul
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
has_mul {x // x.is_block_diagonal}
Equations
- matrix.is_block_diagonal.has_mul = {mul := λ (x y : {x // x.is_block_diagonal}), ⟨↑x.mul ↑y, _⟩}
theorem
matrix.is_block_diagonal.coe_mul
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{x y : {x // x.is_block_diagonal}} :
theorem
matrix.is_block_diagonal.one
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), decidable_eq (s i)] :
@[instance]
def
matrix.is_block_diagonal.has_one
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), decidable_eq (s i)] :
has_one {x // x.is_block_diagonal}
Equations
- matrix.is_block_diagonal.has_one = {one := ⟨1, _⟩}
theorem
matrix.is_block_diagonal.coe_one
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
theorem
matrix.is_block_diagonal.coe_nsmul
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(n : ℕ)
(x : {x // x.is_block_diagonal}) :
theorem
matrix.is_block_diagonal.npow
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(n : ℕ)
{x : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal) :
(x ^ n).is_block_diagonal
@[instance]
def
matrix.is_block_diagonal.has_npow
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
has_pow {x // x.is_block_diagonal} ℕ
Equations
- matrix.is_block_diagonal.has_npow = {pow := λ (x : {x // x.is_block_diagonal}) (n : ℕ), ⟨↑x ^ n, _⟩}
theorem
matrix.is_block_diagonal.coe_npow
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(n : ℕ)
(x : {x // x.is_block_diagonal}) :
@[instance]
def
matrix.is_block_diagonal.semiring
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
semiring {x // x.is_block_diagonal}
Equations
- matrix.is_block_diagonal.semiring = {add := has_add.add (add_zero_class.to_has_add {x // x.is_block_diagonal}), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul add_monoid.has_smul_nat, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul matrix.is_block_diagonal.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (n : ℕ), n • 1, nat_cast_zero := _, nat_cast_succ := _, npow := λ (n : ℕ) (x : {x // x.is_block_diagonal}), x ^ n, npow_zero' := _, npow_succ' := _}
@[instance]
def
matrix.is_block_diagonal.algebra
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
algebra R {x // x.is_block_diagonal}
Equations
- matrix.is_block_diagonal.algebra = {to_has_smul := matrix.has_smul_block_diagonal (λ (i : k) (a b : s i), _inst_5 i a b), to_ring_hom := {to_fun := λ (r : R), r • 1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
theorem
matrix.is_block_diagonal.coe_block_diagonal'_block_diag'
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
(x : {x // x.is_block_diagonal}) :
def
matrix.is_block_diagonal_pi_alg_equiv
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
{x // x.is_block_diagonal} ≃ₐ[R] Π (i : k), matrix (s i) (s i) R
Equations
- matrix.is_block_diagonal_pi_alg_equiv = {to_fun := λ (x : {x // x.is_block_diagonal}), ↑x.block_diag', inv_fun := λ (x : Π (i : k), matrix (s i) (s i) R), ⟨matrix.block_diagonal' x, _⟩, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
matrix.is_block_diagonal_pi_alg_equiv_symm_apply_coe
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : Π (i : k), matrix (s i) (s i) R) :
@[simp]
theorem
matrix.is_block_diagonal_pi_alg_equiv_apply
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : {x // x.is_block_diagonal})
(k_1 : k) :
⇑matrix.is_block_diagonal_pi_alg_equiv x k_1 = ↑x.block_diag' k_1
theorem
matrix.is_block_diagonal.star
{R : Type u_1}
[comm_semiring R]
[star_add_monoid R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
{x : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal) :
@[instance]
def
matrix.is_block_diagonal.has_star
{R : Type u_1}
[comm_semiring R]
[star_add_monoid R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
has_star {x // x.is_block_diagonal}
Equations
- matrix.is_block_diagonal.has_star = {star := λ (x : {x // x.is_block_diagonal}), ⟨x.val.conj_transpose, _⟩}
theorem
matrix.is_block_diagonal.coe_star
{R : Type u_1}
[comm_semiring R]
[star_add_monoid R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : {x // x.is_block_diagonal}) :
↑(has_star.star x) = ↑x.conj_transpose
theorem
matrix.is_block_diagonal_pi_alg_equiv.map_star
{R : Type u_1}
[comm_semiring R]
[star_add_monoid R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : {x // x.is_block_diagonal}) :
theorem
matrix.is_block_diagonal_pi_alg_equiv.symm_map_star
{R : Type u_1}
[comm_semiring R]
[star_add_monoid R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : Π (i : k), matrix (s i) (s i) R) :
Equations
- matrix.equiv.sigma_prod_distrib' β α = let this : (Σ (i : ι), β × α i) ≃ Σ (i : ι), α i × β := equiv.sigma_congr_right (λ (i : ι), equiv.prod_comm β (α i)) in ((equiv.prod_comm β (Σ (i : ι), α i)).trans (equiv.sigma_prod_distrib (λ (i : ι), α i) β)).trans this.symm
Equations
- matrix.sigma_prod_sigma = {to_fun := λ (x : (Σ (i : α), ζ i) × Σ (i : β), ℘ i), ⟨(⇑(equiv.sigma_prod_distrib (λ (i : α), ζ i) (Σ (i : β), ℘ i)) x).fst, ⟨(⇑(matrix.equiv.sigma_prod_distrib' (Σ (i : α), ζ i) (λ (i : β), ℘ i)) x).fst, (x.fst.snd, x.snd.snd)⟩⟩, inv_fun := λ (x : Σ (i : α) (j : β), ζ i × ℘ j), (⟨x.fst, x.snd.snd.fst⟩, ⟨x.snd.fst, x.snd.snd.snd⟩), left_inv := _, right_inv := _}
theorem
matrix.is_block_diagonal.apply_of_ne
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
{x : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal)
(i j : Σ (i : k), s i)
(h : i.fst ≠ j.fst) :
x i j = 0
theorem
matrix.is_block_diagonal.apply_of_ne_coe
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(x : {x // x.is_block_diagonal})
(i j : Σ (i : k), s i)
(h : i.fst ≠ j.fst) :
theorem
matrix.is_block_diagonal.kronecker_mul
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
{x y : matrix (Σ (i : k), s i) (Σ (i : k), s i) R}
(hx : x.is_block_diagonal) :
matrix.is_block_diagonal (λ (i j : Σ (i j : k), s i × s j), matrix.kronecker_map has_mul.mul x y (⇑(matrix.sigma_prod_sigma.symm) i) (⇑(matrix.sigma_prod_sigma.symm) j))
def
matrix.direct_sum_linear_map_alg_equiv_is_block_diagonal_linear_map
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)] :
@[simp]
theorem
matrix.direct_sum_linear_map_alg_equiv_is_block_diagonal_linear_map_symm_apply_apply
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(ᾰ : module.End R {x // x.is_block_diagonal})
(ᾰ_1 : Π (i : k), matrix (s i) (s i) R)
(i : k) :
@[simp]
theorem
matrix.direct_sum_linear_map_alg_equiv_is_block_diagonal_linear_map_apply_apply_coe
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(ᾰ : module.End R (Π (i : k), matrix (s i) (s i) R))
(ᾰ_1 : {x // x.is_block_diagonal}) :
theorem
tensor_product.assoc_include_block
{R : Type u_1}
[comm_semiring R]
{k : Type u_2}
[decidable_eq k]
{s : k → Type u_3}
{i j : k} :
↑((tensor_product.assoc R (Π (a : k), matrix (s a) (s a) R) (Π (a : k), matrix (s a) (s a) R) (Π (a : k), matrix (s a) (s a) R)).symm).comp (tensor_product.map matrix.include_block (tensor_product.map matrix.include_block matrix.include_block)) = (tensor_product.map (tensor_product.map matrix.include_block matrix.include_block) matrix.include_block).comp ↑((tensor_product.assoc R (matrix (s i) (s i) R) (matrix (s j) (s j) R) (matrix (s j) (s j) R)).symm)