# mathlib3documentation

data.matrix.kronecker

# 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 map f : α → β → γ and matrices A and B with coefficients in α and β, respectively, it is defined as the matrix with coefficients in γ such that kronecker_map f A B (i₁, i₂) (j₁, j₂) = f (A i₁ j₁) (B i₁ j₂).
• matrix.kronecker_map_bilinear: when f is bilinear, so is kronecker_map f.

## Specializations #

• matrix.kronecker: An alias of kronecker_map (*). Prefer using the notation.

• matrix.kronecker_bilinear: matrix.kronecker is bilinear

• matrix.kronecker_tmul: An alias of kronecker_map (⊗ₜ). Prefer using the notation.

• matrix.kronecker_tmul_bilinear: matrix.tmul_kronecker is bilinear

## Notations #

These require open_locale kronecker:

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

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

Equations
@[simp]
theorem matrix.kronecker_map_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 : m α) (B : p β) (i : l × n) (j : m × p) :
B i j = f (A i.fst j.fst) (B i.snd j.snd)
theorem matrix.kronecker_map_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 : m α) (B : p β) :
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 : m α) (B : p β) :
(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 : m α) (B : p β) :
(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 : m α) (B : p β) :
B).map g = matrix.kronecker_map (λ (a : α) (b : β), g (f a b)) A B
@[simp]
theorem matrix.kronecker_map_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} [has_zero α] [has_zero γ] (f : α β γ) (hf : (b : β), f 0 b = 0) (B : p β) :
B = 0
@[simp]
theorem matrix.kronecker_map_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} [has_zero β] [has_zero γ] (f : α β γ) (hf : (a : α), f a 0 = 0) (A : m α) :
0 = 0
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₂ : m α) (B : p β) :
(A₁ + A₂) B = B + 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 : m α) (B₁ B₂ : p β) :
(B₁ + B₂) = B₁ + 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} [ α] [ γ] (f : α β γ) (r : R) (hf : (a : α) (b : β), f (r a) b = r f a b) (A : m α) (B : p β) :
(r A) B = r 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} [ β] [ γ] (f : α β γ) (r : R) (hf : (a : α) (b : β), f a (r b) = r f a b) (A : m α) (B : p β) :
(r B) = r 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.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 : m α) (b : n β) :
= 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 : 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) :
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 : m α) (N : p β) :
( em) M) ( ep) N) = (matrix.reindex (el.prod_congr en) (em.prod_congr ep)) 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 : m α) (N : n' β) :
( em) M) N = (matrix.reindex (el.prod_congr (equiv.refl n)) (em.prod_congr (equiv.refl n'))) 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 : l' α) (N : 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 : m α) (B : p β) (D : r δ) (φ : ω ω') (hφ : (a : α) (b : β) (d : δ), φ (g (f a b) d) = f' a (g' b d)) :
((matrix.reindex n q) p r)).trans φ.map_matrix) B) D) = 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 : m α) (B : p β) (D : r δ) (h : (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' b d)) :
(matrix.reindex n q) p r)) B) D) = 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} [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) :
m α →ₗ[R] p β →ₗ[R] matrix (l × n) (m × p) γ

When f is bilinear then matrix.kronecker_map f is also bilinear.

Equations
@[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} [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) (m_1 : m α) (B : p β) :
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} [fintype m] [fintype m'] [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) (h_comm : (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b') (A : m α) (B : n α) (A' : matrix l' m' β) (B' : matrix m' n' β) :
(A.mul B)) (A'.mul B') = ( A').mul ( 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} [fintype m] [fintype n] [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) (A : m α) (B : 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} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] [comm_ring β] [comm_ring γ] [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) (h_comm : (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b') (A : m α) (B : n β) :
( B).det = (A.map (λ (a : α), (f a) 1)).det ^ * (B.map (λ (b : β), (f 1) b)).det ^

determinant of matrix.kronecker_map_bilinear.

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

### Specialization to matrix.kronecker_map (*)#

@[simp]
def matrix.kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [has_mul α] :
m α p α matrix (l × n) (m × p) α

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

Equations
@[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 : m α) (B : p α) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
(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} [semiring α] [ α] :
m α →ₗ[R] p α →ₗ[R] matrix (l × n) (m × p) α

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} (B : p α) :
@[simp]
theorem matrix.kronecker_zero {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (A : m α) :
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₂ : m α) (B : p α) :
(A₁ + 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 : m α) (B₁ B₂ : p α) :
(B₁ + 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 α] [ α] [ α] (r : R) (A : m α) (B : p α) :
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 α] [ α] [ α] (r : R) (A : m α) (B : p α) :
(r B) =
theorem matrix.diagonal_kronecker_diagonal {α : Type u_2} {m : Type u_9} {n : Type u_10} [decidable_eq m] [decidable_eq n] (a : m α) (b : n α) :
= 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} [decidable_eq n] (A : m α) (b : n α) :
theorem matrix.diagonal_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [decidable_eq l] (a : l α) (B : 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} [decidable_eq m] [decidable_eq n] :
theorem matrix.kronecker_one {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [decidable_eq n] (A : m α) :
= 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} [decidable_eq l] (B : 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'] (A : m α) (B : n α) (A' : matrix l' m' α) (B' : matrix m' n' α) :
(A'.mul B') = .mul
@[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 : m α) (B : p α) (C : r α) :
(matrix.reindex n q) p r)) =
theorem matrix.trace_kronecker {α : Type u_2} {m : Type u_9} {n : Type u_10} [fintype m] [fintype n] [semiring α] (A : m α) (B : n α) :
= A.trace * B.trace
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 : m R) (B : n R) :
= A.det ^ * B.det ^
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 : m R) (B : 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} [ α] [ β] :
m α p β matrix (l × n) (m × p) α β)

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

Equations
@[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} [ α] [ β] (A : m α) (B : p β) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
matrix.kronecker_map (λ (_x : α) (_y : β), _x ⊗ₜ[R] _y) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂
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} [ α] [ β] :
m α →ₗ[R] p β →ₗ[R] matrix (l × n) (m × p) α β)

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} [ α] [ β] (B : p β) :
= 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} [ α] [ β] (A : m α) :
= 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} [ α] (A₁ A₂ : m α) (B : p α) :
(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} [ α] (A : m α) (B₁ B₂ : p α) :
(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} [ α] (r : R) (A : m α) (B : p α) :
(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} [ α] (r : R) (A : m α) (B : p α) :
(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} [ α] [decidable_eq m] [decidable_eq n] (a : m α) (b : n α) :
= 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} [ α] [decidable_eq n] (A : m α) (b : n α) :
= 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} [ α] [decidable_eq l] (a : l α) (B : 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} [ α] [ β] [ γ] (A : m α) (B : p β) (C : r γ) :
(matrix.reindex n q) p r)) C).map β γ)) =
theorem matrix.trace_kronecker_tmul (R : Type u_1) {α : Type u_2} {β : Type u_4} {m : Type u_9} {n : Type u_10} [ α] [ β] [fintype m] [fintype n] (A : m α) (B : n β) :
@[simp]
theorem matrix.one_kronecker_tmul_one (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [semiring α] [ α] [decidable_eq m] [decidable_eq n] :
= 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} [semiring α] [semiring β] [ α] [ β] [fintype m] [fintype m'] (A : m α) (B : n α) (A' : matrix l' m' β) (B' : matrix m' n' β) :
(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 β] [ α] [ β] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (A : m α) (B : n β) :
B).det = (A.det ^ ⊗ₜ[R] (B.det ^