# Kronecker product of matrices #

This defines the Kronecker product.

## Main definitions #

• Matrix.kroneckerMap: A generalization of the Kronecker product: given a map f : α → β → γ and matrices A and B with coefficients in α and β, respectively, it is defined as the matrix with coefficients in γ such that kroneckerMap f A B (i₁, i₂) (j₁, j₂) = f (A i₁ j₁) (B i₁ j₂).
• Matrix.kroneckerMapBilinear: when f is bilinear, so is kroneckerMap f.

## Specializations #

• Matrix.kronecker: An alias of kroneckerMap (*). Prefer using the notation.

• Matrix.kroneckerBilinear: Matrix.kronecker is bilinear

• Matrix.kroneckerTMul: An alias of kroneckerMap (⊗ₜ). Prefer using the notation.

• Matrix.kroneckerTMulBilinear: Matrix.kroneckerTMul is bilinear

## Notations #

These require open Kronecker:

• A ⊗ₖ B for kroneckerMap (*) A B. Lemmas about this notation use the token kronecker.
• A ⊗ₖₜ B and A ⊗ₖₜ[R] B for kroneckerMap (⊗ₜ) A B. Lemmas about this notation use the token kroneckerTMul.
def Matrix.kroneckerMap {α : 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} (f : αβγ) (A : Matrix l m α) (B : Matrix n p β) :
Matrix (l × n) (m × p) γ

Produce a matrix with f applied to every pair of elements from A and B.

Equations
• = Matrix.of fun (i : l × n) (j : m × p) => f (A i.1 j.1) (B i.2 j.2)
Instances For
@[simp]
theorem Matrix.kroneckerMap_apply {α : 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} (f : αβγ) (A : Matrix l m α) (B : Matrix n p β) (i : l × n) (j : m × p) :
Matrix.kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2)
theorem Matrix.kroneckerMap_transpose {α : 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} (f : αβγ) (A : Matrix l m α) (B : Matrix n p β) :
Matrix.kroneckerMap f A.transpose B.transpose = ().transpose
theorem Matrix.kroneckerMap_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.kroneckerMap f (A.map g) B = Matrix.kroneckerMap (fun (a : α) (b : β) => f (g a) b) A B
theorem Matrix.kroneckerMap_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.kroneckerMap f A (B.map g) = Matrix.kroneckerMap (fun (a : α) (b : β) => f a (g b)) A B
theorem Matrix.kroneckerMap_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 β) :
().map g = Matrix.kroneckerMap (fun (a : α) (b : β) => g (f a b)) A B
@[simp]
theorem Matrix.kroneckerMap_zero_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} [Zero α] [Zero γ] (f : αβγ) (hf : ∀ (b : β), f 0 b = 0) (B : Matrix n p β) :
= 0
@[simp]
theorem Matrix.kroneckerMap_zero_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} [Zero β] [Zero γ] (f : αβγ) (hf : ∀ (a : α), f a 0 = 0) (A : Matrix l m α) :
= 0
theorem Matrix.kroneckerMap_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} [Add α] [Add γ] (f : αβγ) (hf : ∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b) (A₁ : Matrix l m α) (A₂ : Matrix l m α) (B : Matrix n p β) :
Matrix.kroneckerMap f (A₁ + A₂) B = +
theorem Matrix.kroneckerMap_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} [Add β] [Add γ] (f : αβγ) (hf : ∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂) (A : Matrix l m α) (B₁ : Matrix n p β) (B₂ : Matrix n p β) :
Matrix.kroneckerMap f A (B₁ + B₂) = +
theorem Matrix.kroneckerMap_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} [SMul R α] [SMul R γ] (f : αβγ) (r : R) (hf : ∀ (a : α) (b : β), f (r a) b = r f a b) (A : Matrix l m α) (B : Matrix n p β) :
theorem Matrix.kroneckerMap_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} [SMul R β] [SMul R γ] (f : αβγ) (r : R) (hf : ∀ (a : α) (b : β), f a (r b) = r f a b) (A : Matrix l m α) (B : Matrix n p β) :
theorem Matrix.kroneckerMap_diagonal_diagonal {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [Zero α] [Zero β] [Zero γ] [] [] (f : αβγ) (hf₁ : ∀ (b : β), f 0 b = 0) (hf₂ : ∀ (a : α), f a 0 = 0) (a : mα) (b : nβ) :
= Matrix.diagonal fun (mn : m × n) => f (a mn.1) (b mn.2)
theorem Matrix.kroneckerMap_diagonal_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Zero β] [Zero γ] [] (f : αβγ) (hf : ∀ (a : α), f a 0 = 0) (A : Matrix l m α) (b : nβ) :
= Matrix.blockDiagonal fun (i : n) => A.map fun (a : α) => f a (b i)
theorem Matrix.kroneckerMap_diagonal_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Zero α] [Zero γ] [] (f : αβγ) (hf : ∀ (b : β), f 0 b = 0) (a : lα) (B : Matrix m n β) :
= (Matrix.reindex () ()) (Matrix.blockDiagonal fun (i : l) => B.map fun (b : β) => f (a i) b)
@[simp]
theorem Matrix.kroneckerMap_one_one {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [Zero α] [Zero β] [Zero γ] [One α] [One β] [One γ] [] [] (f : αβγ) (hf₁ : ∀ (b : β), f 0 b = 0) (hf₂ : ∀ (a : α), f a 0 = 0) (hf₃ : f 1 1 = 1) :
= 1
theorem Matrix.kroneckerMap_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.kroneckerMap f ((Matrix.reindex el em) M) ((Matrix.reindex en ep) N) = (Matrix.reindex (el.prodCongr en) (em.prodCongr ep)) ()
theorem Matrix.kroneckerMap_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.kroneckerMap f ((Matrix.reindex el em) M) N = (Matrix.reindex (el.prodCongr ()) (em.prodCongr ())) ()
theorem Matrix.kroneckerMap_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.kroneckerMap f M ((Matrix.reindex em en) N) = (Matrix.reindex (().prodCongr em) (().prodCongr en)) ()
theorem Matrix.kroneckerMap_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_18} {ξ : Type u_19} {ω : Type u_20} {ω' : Type u_21} (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 () ()).trans φ.mapMatrix) (Matrix.kroneckerMap g () D) = Matrix.kroneckerMap f' A ()
theorem Matrix.kroneckerMap_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_18} {ξ : Type u_19} {ω : Type u_20} (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)) :
@[simp]
theorem Matrix.kroneckerMapBilinear_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} [] [] [] [] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (m : Matrix l m✝ α) (B : Matrix n p β) :
() B = Matrix.kroneckerMap (fun (r : α) (s : β) => (f r) s) m B
def Matrix.kroneckerMapBilinear {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} [] [] [] [] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) :
Matrix l m α →ₗ[R] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) γ

When f is bilinear then Matrix.kroneckerMap f is also bilinear.

Equations
Instances For
theorem Matrix.kroneckerMapBilinear_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} [] [] [Fintype m'] [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' β) :
( (A * B)) (A' * B') = () A' * () B'

Matrix.kroneckerMapBilinear commutes with * if f does.

This is primarily used with R = ℕ to prove Matrix.mul_kronecker_mul.

theorem Matrix.trace_kroneckerMapBilinear {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [] [] [] [] [] [] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (A : Matrix m m α) (B : Matrix n n β) :
(() B).trace = (f A.trace) B.trace

trace distributes over Matrix.kroneckerMapBilinear.

This is primarily used with R = ℕ to prove Matrix.trace_kronecker.

theorem Matrix.det_kroneckerMapBilinear {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [] [] [] [] [] [] [] [] [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 β) :
(() B).det = (A.map fun (a : α) => (f a) 1).det ^ * (B.map fun (b : β) => (f 1) b).det ^

determinant of Matrix.kroneckerMapBilinear.

This is primarily used with R = ℕ to prove Matrix.det_kronecker.

### Specialization to Matrix.kroneckerMap (*)#

def Matrix.kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Mul α] :
Matrix l m αMatrix n p αMatrix (l × n) (m × p) α

The Kronecker product. This is just a shorthand for kroneckerMap (*). Prefer the notation ⊗ₖ rather than this definition.

Equations
Instances For
Equations
Instances For
@[simp]
theorem Matrix.kronecker_apply {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Mul α] (A : Matrix l m α) (B : Matrix n p α) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂
def Matrix.kroneckerBilinear {R : Type u_1} {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [] [] [Algebra R α] :
Matrix l m α →ₗ[R] Matrix n p α →ₗ[R] Matrix (l × n) (m × p) α

Matrix.kronecker as a bilinear map.

Equations
Instances For

What follows is a copy, in order, of every Matrix.kroneckerMap lemma above that has hypotheses which can be filled by properties of *.

theorem Matrix.zero_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [] (B : Matrix n p α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) 0 B = 0
theorem Matrix.kronecker_zero {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [] (A : Matrix l m α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) 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} [] (A₁ : Matrix l m α) (A₂ : Matrix l m α) (B : Matrix n p α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) (A₁ + A₂) B = Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A₁ B + Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) 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} [] (A : Matrix l m α) (B₁ : Matrix n p α) (B₂ : Matrix n p α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A (B₁ + B₂) = Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B₁ + Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) 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} [] [] [] [] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) (r A) B = r Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) 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} [] [] [] [] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A (r B) = r Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B
theorem Matrix.diagonal_kronecker_diagonal {α : Type u_2} {m : Type u_9} {n : Type u_10} [] [] [] (a : mα) (b : nα) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) () () = Matrix.diagonal fun (mn : m × n) => a mn.1 * b mn.2
theorem Matrix.kronecker_diagonal {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (A : Matrix l m α) (b : nα) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A () = Matrix.blockDiagonal fun (i : n) => MulOpposite.op (b i) A
theorem Matrix.diagonal_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (a : lα) (B : Matrix m n α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) () B = (Matrix.reindex () ()) (Matrix.blockDiagonal fun (i : l) => a i B)
@[simp]
theorem Matrix.natCast_kronecker_natCast {α : Type u_2} {m : Type u_9} {n : Type u_10} [] [] [] (a : ) (b : ) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) a b = (a * b)
theorem Matrix.kronecker_natCast {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (A : Matrix l m α) (b : ) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A b = Matrix.blockDiagonal fun (x : n) => b A
theorem Matrix.natCast_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (a : ) (B : Matrix m n α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) (a) B = (Matrix.reindex () ()) (Matrix.blockDiagonal fun (x : l) => a B)
theorem Matrix.kronecker_ofNat {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (A : Matrix l m α) (b : ) [b.AtLeastTwo] :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A () = Matrix.blockDiagonal fun (x : n) =>
theorem Matrix.ofNat_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (a : ) [a.AtLeastTwo] (B : Matrix m n α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) () B = (Matrix.reindex () ()) (Matrix.blockDiagonal fun (x : l) => B)
theorem Matrix.one_kronecker_one {α : Type u_2} {m : Type u_9} {n : Type u_10} [] [] [] :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) 1 1 = 1
theorem Matrix.kronecker_one {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (A : Matrix l m α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A 1 = Matrix.blockDiagonal fun (x : n) => A
theorem Matrix.one_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] (B : Matrix m n α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) 1 B = (Matrix.reindex () ()) (Matrix.blockDiagonal fun (x : 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'] [] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' α) (B' : Matrix m' n' α) :
Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) (A * B) (A' * B') = Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A A' * Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) B B'
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} [] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
(Matrix.reindex () ()) (Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) (Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B) C) = Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A (Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) B C)
@[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} [] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
(Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) (Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B) C).submatrix ().symm ().symm = Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A (Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) B C)
theorem Matrix.trace_kronecker {α : Type u_2} {m : Type u_9} {n : Type u_10} [] [] [] (A : Matrix m m α) (B : Matrix n n α) :
(Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B).trace = A.trace * B.trace
theorem Matrix.det_kronecker {R : Type u_1} {m : Type u_9} {n : Type u_10} [] [] [] [] [] (A : Matrix m m R) (B : Matrix n n R) :
(Matrix.kroneckerMap (fun (x x_1 : R) => x * x_1) A B).det = A.det ^ * B.det ^
theorem Matrix.inv_kronecker {R : Type u_1} {m : Type u_9} {n : Type u_10} [] [] [] [] [] (A : Matrix m m R) (B : Matrix n n R) :
(Matrix.kroneckerMap (fun (x x_1 : R) => x * x_1) A B)⁻¹ = Matrix.kroneckerMap (fun (x x_1 : R) => x * x_1) A⁻¹ B⁻¹

### Specialization to Matrix.kroneckerMap (⊗ₜ)#

noncomputable def Matrix.kroneckerTMul (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} [] [] [] [Module R α] [Module R β] :
Matrix l m αMatrix n p βMatrix (l × n) (m × p) ()

The Kronecker tensor product. This is just a shorthand for kroneckerMap (⊗ₜ). Prefer the notation ⊗ₖₜ rather than this definition.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Matrix.kroneckerTMul_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} [] [] [] [Module R α] [Module R β] (A : Matrix l m α) (B : Matrix n p β) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
Matrix.kroneckerMap (fun (x : α) (x_1 : β) => x ⊗ₜ[R] x_1) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂
noncomputable def Matrix.kroneckerTMulBilinear (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} [] [] [] [Module R α] [Module R β] :
Matrix l m α →ₗ[R] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) ()

Matrix.kronecker as a bilinear map.

Equations
Instances For

What follows is a copy, in order, of every Matrix.kroneckerMap lemma above that has hypotheses which can be filled by properties of ⊗ₜ.

theorem Matrix.zero_kroneckerTMul (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} [] [] [] [Module R α] [Module R β] (B : Matrix n p β) :
= 0
theorem Matrix.kroneckerTMul_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} [] [] [] [Module R α] [Module R β] (A : Matrix l m α) :
= 0
theorem Matrix.add_kroneckerTMul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [] [] [Module R α] (A₁ : Matrix l m α) (A₂ : Matrix l m α) (B : Matrix n p α) :
Matrix.kroneckerMap (A₁ + A₂) B = Matrix.kroneckerMap (fun (x x_1 : α) => x ⊗ₜ[R] x_1) A₁ B + Matrix.kroneckerMap (fun (x x_1 : α) => x ⊗ₜ[R] x_1) A₂ B
theorem Matrix.kroneckerTMul_add (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [] [] [Module R α] (A : Matrix l m α) (B₁ : Matrix n p α) (B₂ : Matrix n p α) :
Matrix.kroneckerMap A (B₁ + B₂) = Matrix.kroneckerMap (fun (x x_1 : α) => x ⊗ₜ[R] x_1) A B₁ + Matrix.kroneckerMap (fun (x x_1 : α) => x ⊗ₜ[R] x_1) A B₂
theorem Matrix.smul_kroneckerTMul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [] [] [Module R α] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
Matrix.kroneckerMap (r A) B = r Matrix.kroneckerMap (fun (x x_1 : α) => x ⊗ₜ[R] x_1) A B
theorem Matrix.kroneckerTMul_smul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [] [] [Module R α] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
Matrix.kroneckerMap A (r B) = r Matrix.kroneckerMap (fun (x x_1 : α) => x ⊗ₜ[R] x_1) A B
theorem Matrix.diagonal_kroneckerTMul_diagonal (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [] [] [Module R α] [] [] (a : mα) (b : nα) :
= Matrix.diagonal fun (mn : m × n) => a mn.1 ⊗ₜ[R] b mn.2
theorem Matrix.kroneckerTMul_diagonal (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] [Module R α] [] (A : Matrix l m α) (b : nα) :
= Matrix.blockDiagonal fun (i : n) => A.map fun (a : α) => a ⊗ₜ[R] b i
theorem Matrix.diagonal_kroneckerTMul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [] [] [Module R α] [] (a : lα) (B : Matrix m n α) :
= (Matrix.reindex () ()) (Matrix.blockDiagonal fun (i : l) => B.map fun (b : α) => a i ⊗ₜ[R] b)
theorem Matrix.kroneckerTMul_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} [] [] [] [] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
(Matrix.reindex () ()) (().map ()) =
@[simp]
theorem Matrix.kroneckerTMul_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} [] [] [] [] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
(().map ()).submatrix ().symm ().symm =
theorem Matrix.trace_kroneckerTMul (R : Type u_1) {α : Type u_2} {β : Type u_4} {m : Type u_9} {n : Type u_10} [] [] [] [Module R α] [Module R β] [] [] (A : Matrix m m α) (B : Matrix n n β) :
().trace = A.trace ⊗ₜ[R] B.trace
@[simp]
theorem Matrix.one_kroneckerTMul_one (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [] [] [Algebra R α] [] [] :
= 1
theorem Matrix.mul_kroneckerTMul_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} [] [] [] [Algebra R α] [Algebra R β] [] [Fintype m'] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) :
Matrix.kroneckerMap (A * B) (A' * B') = *
theorem Matrix.det_kroneckerTMul (R : Type u_1) {α : Type u_2} {β : Type u_4} {m : Type u_9} {n : Type u_10} [] [] [] [Algebra R α] [Algebra R β] [] [] [] [] (A : Matrix m m α) (B : Matrix n n β) :
().det = (A.det ^ ) ⊗ₜ[R] (B.det ^ )