Kronecker product of matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This defines the Kronecker product.
Main definitions #
matrix.kronecker_map: A generalization of the Kronecker product: given a mapf : α → β → γand matricesAandBwith coefficients inαandβ, respectively, it is defined as the matrix with coefficients inγsuch thatkronecker_map f A B (i₁, i₂) (j₁, j₂) = f (A i₁ j₁) (B i₁ j₂).matrix.kronecker_map_bilinear: whenfis bilinear, so iskronecker_map f.
Specializations #
-
matrix.kronecker: An alias ofkronecker_map (*). Prefer using the notation. -
matrix.kronecker_bilinear:matrix.kroneckeris bilinear -
matrix.kronecker_tmul: An alias ofkronecker_map (⊗ₜ). Prefer using the notation. -
matrix.kronecker_tmul_bilinear:matrix.tmul_kroneckeris bilinear
Notations #
These require open_locale kronecker:
A ⊗ₖ Bforkronecker_map (*) A B. Lemmas about this notation use the tokenkronecker.A ⊗ₖₜ BandA ⊗ₖₜ[R] Bforkronecker_map (⊗ₜ) A B. Lemmas about this notation use the tokenkronecker_tmul.
@[simp]
theorem
matrix.kronecker_map_map_left
{α : Type u_2}
{α' : Type u_3}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
(f : α' → β → γ)
(g : α → α')
(A : matrix l m α)
(B : matrix n p β) :
matrix.kronecker_map f (A.map g) B = matrix.kronecker_map (λ (a : α) (b : β), f (g a) b) A B
theorem
matrix.kronecker_map_map_right
{α : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
(f : α → β' → γ)
(g : β → β')
(A : matrix l m α)
(B : matrix n p β) :
matrix.kronecker_map f A (B.map g) = matrix.kronecker_map (λ (a : α) (b : β), f a (g b)) A B
theorem
matrix.kronecker_map_map
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{γ' : Type u_7}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
(f : α → β → γ)
(g : γ → γ')
(A : matrix l m α)
(B : matrix n p β) :
(matrix.kronecker_map f A B).map g = matrix.kronecker_map (λ (a : α) (b : β), g (f a b)) A B
theorem
matrix.kronecker_map_add_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[has_add α]
[has_add γ]
(f : α → β → γ)
(hf : ∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b)
(A₁ A₂ : matrix l m α)
(B : matrix n p β) :
matrix.kronecker_map f (A₁ + A₂) B = matrix.kronecker_map f A₁ B + matrix.kronecker_map f A₂ B
theorem
matrix.kronecker_map_add_right
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[has_add β]
[has_add γ]
(f : α → β → γ)
(hf : ∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂)
(A : matrix l m α)
(B₁ B₂ : matrix n p β) :
matrix.kronecker_map f A (B₁ + B₂) = matrix.kronecker_map f A B₁ + matrix.kronecker_map f A B₂
theorem
matrix.kronecker_map_smul_left
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[has_smul R α]
[has_smul R γ]
(f : α → β → γ)
(r : R)
(hf : ∀ (a : α) (b : β), f (r • a) b = r • f a b)
(A : matrix l m α)
(B : matrix n p β) :
matrix.kronecker_map f (r • A) B = r • matrix.kronecker_map f A B
theorem
matrix.kronecker_map_smul_right
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[has_smul R β]
[has_smul R γ]
(f : α → β → γ)
(r : R)
(hf : ∀ (a : α) (b : β), f a (r • b) = r • f a b)
(A : matrix l m α)
(B : matrix n p β) :
matrix.kronecker_map f A (r • B) = r • matrix.kronecker_map f A B
theorem
matrix.kronecker_map_diagonal_diagonal
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[has_zero α]
[has_zero β]
[has_zero γ]
[decidable_eq m]
[decidable_eq n]
(f : α → β → γ)
(hf₁ : ∀ (b : β), f 0 b = 0)
(hf₂ : ∀ (a : α), f a 0 = 0)
(a : m → α)
(b : n → β) :
matrix.kronecker_map f (matrix.diagonal a) (matrix.diagonal b) = matrix.diagonal (λ (mn : m × n), f (a mn.fst) (b mn.snd))
theorem
matrix.kronecker_map_diagonal_right
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[has_zero β]
[has_zero γ]
[decidable_eq n]
(f : α → β → γ)
(hf : ∀ (a : α), f a 0 = 0)
(A : matrix l m α)
(b : n → β) :
matrix.kronecker_map f A (matrix.diagonal b) = matrix.block_diagonal (λ (i : n), A.map (λ (a : α), f a (b i)))
theorem
matrix.kronecker_map_diagonal_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[has_zero α]
[has_zero γ]
[decidable_eq l]
(f : α → β → γ)
(hf : ∀ (b : β), f 0 b = 0)
(a : l → α)
(B : matrix m n β) :
matrix.kronecker_map f (matrix.diagonal a) B = ⇑(matrix.reindex (equiv.prod_comm m l) (equiv.prod_comm n l)) (matrix.block_diagonal (λ (i : l), B.map (λ (b : β), f (a i) b)))
@[simp]
theorem
matrix.kronecker_map_one_one
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[has_zero α]
[has_zero β]
[has_zero γ]
[has_one α]
[has_one β]
[has_one γ]
[decidable_eq m]
[decidable_eq n]
(f : α → β → γ)
(hf₁ : ∀ (b : β), f 0 b = 0)
(hf₂ : ∀ (a : α), f a 0 = 0)
(hf₃ : f 1 1 = 1) :
matrix.kronecker_map f 1 1 = 1
theorem
matrix.kronecker_map_reindex
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
{l' : Type u_14}
{m' : Type u_15}
{n' : Type u_16}
{p' : Type u_17}
(f : α → β → γ)
(el : l ≃ l')
(em : m ≃ m')
(en : n ≃ n')
(ep : p ≃ p')
(M : matrix l m α)
(N : matrix n p β) :
matrix.kronecker_map f (⇑(matrix.reindex el em) M) (⇑(matrix.reindex en ep) N) = ⇑(matrix.reindex (el.prod_congr en) (em.prod_congr ep)) (matrix.kronecker_map f M N)
theorem
matrix.kronecker_map_reindex_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{l' : Type u_14}
{m' : Type u_15}
{n' : Type u_16}
(f : α → β → γ)
(el : l ≃ l')
(em : m ≃ m')
(M : matrix l m α)
(N : matrix n n' β) :
matrix.kronecker_map f (⇑(matrix.reindex el em) M) N = ⇑(matrix.reindex (el.prod_congr (equiv.refl n)) (em.prod_congr (equiv.refl n'))) (matrix.kronecker_map f M N)
theorem
matrix.kronecker_map_reindex_right
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{l' : Type u_14}
{m' : Type u_15}
{n' : Type u_16}
(f : α → β → γ)
(em : m ≃ m')
(en : n ≃ n')
(M : matrix l l' α)
(N : matrix m n β) :
matrix.kronecker_map f M (⇑(matrix.reindex em en) N) = ⇑(matrix.reindex ((equiv.refl l).prod_congr em) ((equiv.refl l').prod_congr en)) (matrix.kronecker_map f M N)
theorem
matrix.kronecker_map_assoc
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
{q : Type u_12}
{r : Type u_13}
{δ : Type u_1}
{ξ : Type u_3}
{ω : Type u_5}
{ω' : Type u_7}
(f : α → β → γ)
(g : γ → δ → ω)
(f' : α → ξ → ω')
(g' : β → δ → ξ)
(A : matrix l m α)
(B : matrix n p β)
(D : matrix q r δ)
(φ : ω ≃ ω')
(hφ : ∀ (a : α) (b : β) (d : δ), ⇑φ (g (f a b) d) = f' a (g' b d)) :
⇑((matrix.reindex (equiv.prod_assoc l n q) (equiv.prod_assoc m p r)).trans φ.map_matrix) (matrix.kronecker_map g (matrix.kronecker_map f A B) D) = matrix.kronecker_map f' A (matrix.kronecker_map g' B D)
theorem
matrix.kronecker_map_assoc₁
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
{q : Type u_12}
{r : Type u_13}
{δ : Type u_1}
{ξ : Type u_3}
{ω : Type u_5}
(f : α → β → γ)
(g : γ → δ → ω)
(f' : α → ξ → ω)
(g' : β → δ → ξ)
(A : matrix l m α)
(B : matrix n p β)
(D : matrix q r δ)
(h : ∀ (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' b d)) :
⇑(matrix.reindex (equiv.prod_assoc l n q) (equiv.prod_assoc m p r)) (matrix.kronecker_map g (matrix.kronecker_map f A B) D) = matrix.kronecker_map f' A (matrix.kronecker_map g' B D)
def
matrix.kronecker_map_bilinear
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[add_comm_monoid γ]
[module R α]
[module R β]
[module R γ]
(f : α →ₗ[R] β →ₗ[R] γ) :
When f is bilinear then matrix.kronecker_map f is also bilinear.
Equations
- matrix.kronecker_map_bilinear f = linear_map.mk₂ R (matrix.kronecker_map (λ (r : α) (s : β), ⇑(⇑f r) s)) _ _ _ _
@[simp]
theorem
matrix.kronecker_map_bilinear_apply_apply
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[add_comm_monoid γ]
[module R α]
[module R β]
[module R γ]
(f : α →ₗ[R] β →ₗ[R] γ)
(m_1 : matrix l m α)
(B : matrix n p β) :
⇑(⇑(matrix.kronecker_map_bilinear f) m_1) B = matrix.kronecker_map (λ (r : α), ⇑(⇑f r)) m_1 B
theorem
matrix.kronecker_map_bilinear_mul_mul
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{l' : Type u_14}
{m' : Type u_15}
{n' : Type u_16}
[comm_semiring R]
[fintype m]
[fintype m']
[non_unital_non_assoc_semiring α]
[non_unital_non_assoc_semiring β]
[non_unital_non_assoc_semiring γ]
[module R α]
[module R β]
[module R γ]
(f : α →ₗ[R] β →ₗ[R] γ)
(h_comm : ∀ (a b : α) (a' b' : β), ⇑(⇑f (a * b)) (a' * b') = ⇑(⇑f a) a' * ⇑(⇑f b) b')
(A : matrix l m α)
(B : matrix m n α)
(A' : matrix l' m' β)
(B' : matrix m' n' β) :
⇑(⇑(matrix.kronecker_map_bilinear f) (A.mul B)) (A'.mul B') = (⇑(⇑(matrix.kronecker_map_bilinear f) A) A').mul (⇑(⇑(matrix.kronecker_map_bilinear f) B) B')
matrix.kronecker_map_bilinear commutes with ⬝ if f commutes with *.
This is primarily used with R = ℕ to prove matrix.mul_kronecker_mul.
theorem
matrix.trace_kronecker_map_bilinear
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[comm_semiring R]
[fintype m]
[fintype n]
[add_comm_monoid α]
[add_comm_monoid β]
[add_comm_monoid γ]
[module R α]
[module R β]
[module R γ]
(f : α →ₗ[R] β →ₗ[R] γ)
(A : matrix m m α)
(B : matrix n n β) :
trace distributes over matrix.kronecker_map_bilinear.
This is primarily used with R = ℕ to prove matrix.trace_kronecker.
theorem
matrix.det_kronecker_map_bilinear
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[comm_semiring R]
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
[comm_ring β]
[comm_ring γ]
[module R α]
[module R β]
[module R γ]
(f : α →ₗ[R] β →ₗ[R] γ)
(h_comm : ∀ (a b : α) (a' b' : β), ⇑(⇑f (a * b)) (a' * b') = ⇑(⇑f a) a' * ⇑(⇑f b) b')
(A : matrix m m α)
(B : matrix n n β) :
determinant of matrix.kronecker_map_bilinear.
This is primarily used with R = ℕ to prove matrix.det_kronecker.
Specialization to matrix.kronecker_map (*) #
@[simp]
theorem
matrix.kronecker_apply
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[has_mul α]
(A : matrix l m α)
(B : matrix n p α)
(i₁ : l)
(i₂ : n)
(j₁ : m)
(j₂ : p) :
matrix.kronecker_map has_mul.mul A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂
def
matrix.kronecker_bilinear
{R : Type u_1}
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[semiring α]
[algebra R α] :
matrix.kronecker as a bilinear map.
Equations
What follows is a copy, in order, of every matrix.kronecker_map lemma above that has
hypotheses which can be filled by properties of *.
@[simp]
theorem
matrix.zero_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[mul_zero_class α]
(B : matrix n p α) :
matrix.kronecker_map has_mul.mul 0 B = 0
@[simp]
theorem
matrix.kronecker_zero
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[mul_zero_class α]
(A : matrix l m α) :
matrix.kronecker_map has_mul.mul A 0 = 0
theorem
matrix.add_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[distrib α]
(A₁ A₂ : matrix l m α)
(B : matrix n p α) :
matrix.kronecker_map has_mul.mul (A₁ + A₂) B = matrix.kronecker_map has_mul.mul A₁ B + matrix.kronecker_map has_mul.mul A₂ B
theorem
matrix.kronecker_add
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[distrib α]
(A : matrix l m α)
(B₁ B₂ : matrix n p α) :
matrix.kronecker_map has_mul.mul A (B₁ + B₂) = matrix.kronecker_map has_mul.mul A B₁ + matrix.kronecker_map has_mul.mul A B₂
theorem
matrix.smul_kronecker
{R : Type u_1}
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[monoid R]
[monoid α]
[mul_action R α]
[is_scalar_tower R α α]
(r : R)
(A : matrix l m α)
(B : matrix n p α) :
matrix.kronecker_map has_mul.mul (r • A) B = r • matrix.kronecker_map has_mul.mul A B
theorem
matrix.kronecker_smul
{R : Type u_1}
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[monoid R]
[monoid α]
[mul_action R α]
[smul_comm_class R α α]
(r : R)
(A : matrix l m α)
(B : matrix n p α) :
matrix.kronecker_map has_mul.mul A (r • B) = r • matrix.kronecker_map has_mul.mul A B
theorem
matrix.diagonal_kronecker_diagonal
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[mul_zero_class α]
[decidable_eq m]
[decidable_eq n]
(a : m → α)
(b : n → α) :
matrix.kronecker_map has_mul.mul (matrix.diagonal a) (matrix.diagonal b) = matrix.diagonal (λ (mn : m × n), a mn.fst * b mn.snd)
theorem
matrix.kronecker_diagonal
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[mul_zero_class α]
[decidable_eq n]
(A : matrix l m α)
(b : n → α) :
matrix.kronecker_map has_mul.mul A (matrix.diagonal b) = matrix.block_diagonal (λ (i : n), mul_opposite.op (b i) • A)
theorem
matrix.diagonal_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[mul_zero_class α]
[decidable_eq l]
(a : l → α)
(B : matrix m n α) :
matrix.kronecker_map has_mul.mul (matrix.diagonal a) B = ⇑(matrix.reindex (equiv.prod_comm m l) (equiv.prod_comm n l)) (matrix.block_diagonal (λ (i : l), a i • B))
@[simp]
theorem
matrix.one_kronecker_one
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[mul_zero_one_class α]
[decidable_eq m]
[decidable_eq n] :
matrix.kronecker_map has_mul.mul 1 1 = 1
theorem
matrix.kronecker_one
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[mul_zero_one_class α]
[decidable_eq n]
(A : matrix l m α) :
matrix.kronecker_map has_mul.mul A 1 = matrix.block_diagonal (λ (i : n), A)
theorem
matrix.one_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[mul_zero_one_class α]
[decidable_eq l]
(B : matrix m n α) :
matrix.kronecker_map has_mul.mul 1 B = ⇑(matrix.reindex (equiv.prod_comm m l) (equiv.prod_comm n l)) (matrix.block_diagonal (λ (i : l), B))
theorem
matrix.mul_kronecker_mul
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{l' : Type u_14}
{m' : Type u_15}
{n' : Type u_16}
[fintype m]
[fintype m']
[comm_semiring α]
(A : matrix l m α)
(B : matrix m n α)
(A' : matrix l' m' α)
(B' : matrix m' n' α) :
matrix.kronecker_map has_mul.mul (A.mul B) (A'.mul B') = (matrix.kronecker_map has_mul.mul A A').mul (matrix.kronecker_map has_mul.mul B B')
@[simp]
theorem
matrix.kronecker_assoc
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
{q : Type u_12}
{r : Type u_13}
[semigroup α]
(A : matrix l m α)
(B : matrix n p α)
(C : matrix q r α) :
⇑(matrix.reindex (equiv.prod_assoc l n q) (equiv.prod_assoc m p r)) (matrix.kronecker_map has_mul.mul (matrix.kronecker_map has_mul.mul A B) C) = matrix.kronecker_map has_mul.mul A (matrix.kronecker_map has_mul.mul B C)
theorem
matrix.det_kronecker
{R : Type u_1}
{m : Type u_9}
{n : Type u_10}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring R]
(A : matrix m m R)
(B : matrix n n R) :
(matrix.kronecker_map has_mul.mul A B).det = A.det ^ fintype.card n * B.det ^ fintype.card m
theorem
matrix.inv_kronecker
{R : Type u_1}
{m : Type u_9}
{n : Type u_10}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring R]
(A : matrix m m R)
(B : matrix n n R) :
Specialization to matrix.kronecker_map (⊗ₜ) #
@[simp]
def
matrix.kronecker_tmul
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[module R α]
[module R β] :
The Kronecker tensor product. This is just a shorthand for kronecker_map (⊗ₜ).
Prefer the notation ⊗ₖₜ rather than this definition.
Equations
- matrix.kronecker_tmul R = matrix.kronecker_map (λ (_x : α) (_y : β), _x ⊗ₜ[R] _y)
@[simp]
theorem
matrix.kronecker_tmul_apply
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[module R α]
[module R β]
(A : matrix l m α)
(B : matrix n p β)
(i₁ : l)
(i₂ : n)
(j₁ : m)
(j₂ : p) :
def
matrix.kronecker_tmul_bilinear
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[module R α]
[module R β] :
matrix.kronecker as a bilinear map.
Equations
What follows is a copy, in order, of every matrix.kronecker_map lemma above that has
hypotheses which can be filled by properties of ⊗ₜ.
@[simp]
theorem
matrix.zero_kronecker_tmul
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[module R α]
[module R β]
(B : matrix n p β) :
matrix.kronecker_map (tensor_product.tmul R) 0 B = 0
@[simp]
theorem
matrix.kronecker_tmul_zero
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[module R α]
[module R β]
(A : matrix l m α) :
matrix.kronecker_map (tensor_product.tmul R) A 0 = 0
theorem
matrix.add_kronecker_tmul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[module R α]
(A₁ A₂ : matrix l m α)
(B : matrix n p α) :
matrix.kronecker_map (tensor_product.tmul R) (A₁ + A₂) B = matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A₁ B + matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A₂ B
theorem
matrix.kronecker_tmul_add
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[module R α]
(A : matrix l m α)
(B₁ B₂ : matrix n p α) :
matrix.kronecker_map (tensor_product.tmul R) A (B₁ + B₂) = matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B₁ + matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B₂
theorem
matrix.smul_kronecker_tmul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[module R α]
(r : R)
(A : matrix l m α)
(B : matrix n p α) :
matrix.kronecker_map (tensor_product.tmul R) (r • A) B = r • matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B
theorem
matrix.kronecker_tmul_smul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[comm_semiring R]
[add_comm_monoid α]
[module R α]
(r : R)
(A : matrix l m α)
(B : matrix n p α) :
matrix.kronecker_map (tensor_product.tmul R) A (r • B) = r • matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B
theorem
matrix.diagonal_kronecker_tmul_diagonal
(R : Type u_1)
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[comm_semiring R]
[add_comm_monoid α]
[module R α]
[decidable_eq m]
[decidable_eq n]
(a : m → α)
(b : n → α) :
matrix.kronecker_map (tensor_product.tmul R) (matrix.diagonal a) (matrix.diagonal b) = matrix.diagonal (λ (mn : m × n), a mn.fst ⊗ₜ[R] b mn.snd)
theorem
matrix.kronecker_tmul_diagonal
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[comm_semiring R]
[add_comm_monoid α]
[module R α]
[decidable_eq n]
(A : matrix l m α)
(b : n → α) :
matrix.kronecker_map (tensor_product.tmul R) A (matrix.diagonal b) = matrix.block_diagonal (λ (i : n), A.map (λ (a : α), a ⊗ₜ[R] b i))
theorem
matrix.diagonal_kronecker_tmul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[comm_semiring R]
[add_comm_monoid α]
[module R α]
[decidable_eq l]
(a : l → α)
(B : matrix m n α) :
matrix.kronecker_map (tensor_product.tmul R) (matrix.diagonal a) B = ⇑(matrix.reindex (equiv.prod_comm m l) (equiv.prod_comm n l)) (matrix.block_diagonal (λ (i : l), B.map (λ (b : α), a i ⊗ₜ[R] b)))
@[simp]
theorem
matrix.kronecker_tmul_assoc
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
{q : Type u_12}
{r : Type u_13}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[add_comm_monoid γ]
[module R α]
[module R β]
[module R γ]
(A : matrix l m α)
(B : matrix n p β)
(C : matrix q r γ) :
⇑(matrix.reindex (equiv.prod_assoc l n q) (equiv.prod_assoc m p r)) ((matrix.kronecker_map (tensor_product.tmul R) (matrix.kronecker_map (tensor_product.tmul R) A B) C).map ⇑(tensor_product.assoc R α β γ)) = matrix.kronecker_map (tensor_product.tmul R) A (matrix.kronecker_map (tensor_product.tmul R) B C)
theorem
matrix.trace_kronecker_tmul
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{m : Type u_9}
{n : Type u_10}
[comm_semiring R]
[add_comm_monoid α]
[add_comm_monoid β]
[module R α]
[module R β]
[fintype m]
[fintype n]
(A : matrix m m α)
(B : matrix n n β) :
(matrix.kronecker_map (tensor_product.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace
@[simp]
theorem
matrix.one_kronecker_tmul_one
(R : Type u_1)
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[comm_semiring R]
[semiring α]
[algebra R α]
[decidable_eq m]
[decidable_eq n] :
matrix.kronecker_map (tensor_product.tmul R) 1 1 = 1
theorem
matrix.mul_kronecker_tmul_mul
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{l' : Type u_14}
{m' : Type u_15}
{n' : Type u_16}
[comm_semiring R]
[semiring α]
[semiring β]
[algebra R α]
[algebra R β]
[fintype m]
[fintype m']
(A : matrix l m α)
(B : matrix m n α)
(A' : matrix l' m' β)
(B' : matrix m' n' β) :
matrix.kronecker_map (tensor_product.tmul R) (A.mul B) (A'.mul B') = (matrix.kronecker_map (λ (_x : α) (_y : β), _x ⊗ₜ[R] _y) A A').mul (matrix.kronecker_map (λ (_x : α) (_y : β), _x ⊗ₜ[R] _y) B B')
theorem
matrix.det_kronecker_tmul
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{m : Type u_9}
{n : Type u_10}
[comm_ring R]
[comm_ring α]
[comm_ring β]
[algebra R α]
[algebra R β]
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
(A : matrix m m α)
(B : matrix n n β) :
(matrix.kronecker_map (tensor_product.tmul R) A B).det = (A.det ^ fintype.card n) ⊗ₜ[R] (B.det ^ fintype.card m)