[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
⊢ kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.fst) (b mn.snd)
[PROOFSTEP]
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun mn => f (a mn.fst) (b mn.snd)) (i₁, i₂) (j₁, j₂)
[PROOFSTEP]
simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
⊢ kroneckerMap f A (diagonal b) = blockDiagonal fun i => map A fun a => f a (b i)
[PROOFSTEP]
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
i₁ : l
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) = blockDiagonal (fun i => map A fun a => f a (b i)) (i₁, i₂) (j₁, j₂)
[PROOFSTEP]
simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
⊢ kroneckerMap f (diagonal a) B =
    ↑(reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => map B fun b => f (a i) b)
[PROOFSTEP]
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    ↑(reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => map B fun b => f (a i) b) (i₁, i₂)
      (j₁, j₂)
[PROOFSTEP]
simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁷ : Zero α
inst✝⁶ : Zero β
inst✝⁵ : Zero γ
inst✝⁴ : One α
inst✝³ : One β
inst✝² : One γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
hf₃ : f 1 1 = 1
⊢ (diagonal fun mn => f 1 1) = 1
[PROOFSTEP]
simp only [hf₃, diagonal_one]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
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 β
⊢ kroneckerMap f (↑(reindex el em) M) (↑(reindex en ep) N) =
    ↑(reindex (Equiv.prodCongr el en) (Equiv.prodCongr em ep)) (kroneckerMap f M N)
[PROOFSTEP]
ext ⟨i, i'⟩ ⟨j, j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
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 β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f (↑(reindex el em) M) (↑(reindex en ep) N) (i, i') (j, j') =
    ↑(reindex (Equiv.prodCongr el en) (Equiv.prodCongr em ep)) (kroneckerMap f M N) (i, i') (j, j')
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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' β
⊢ ↑(↑(kroneckerMapBilinear f) (A * B)) (A' * B') = ↑(↑(kroneckerMapBilinear f) A) A' * ↑(↑(kroneckerMapBilinear f) B) B'
[PROOFSTEP]
ext ⟨i, i'⟩ ⟨j, j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑(kroneckerMapBilinear f) (A * B)) (A' * B') (i, i') (j, j') =
    (↑(↑(kroneckerMapBilinear f) A) A' * ↑(↑(kroneckerMapBilinear f) B) B') (i, i') (j, j')
[PROOFSTEP]
simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product,
  kroneckerMap_apply]
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑f (Finset.sum Finset.univ fun j_1 => A i j_1 * B j_1 j)) (Finset.sum Finset.univ fun j => A' i' j * B' j j') =
    Finset.sum Finset.univ fun x =>
      Finset.sum Finset.univ fun x_1 => ↑(↑f (A i x)) (A' i' x_1) * ↑(↑f (B x j)) (B' x_1 j')
[PROOFSTEP]
simp_rw [f.map_sum, LinearMap.sum_apply, LinearMap.map_sum, h_comm]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : AddCommMonoid γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
A : Matrix m m α
B : Matrix n n β
⊢ trace (↑(↑(kroneckerMapBilinear f) A) B) = ↑(↑f (trace A)) (trace B)
[PROOFSTEP]
simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂, map_sum, ←
  Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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 β
⊢ det (↑(↑(kroneckerMapBilinear f) A) B) = det (↑(↑(kroneckerMapBilinear f) A) 1 * ↑(↑(kroneckerMapBilinear f) 1) B)
[PROOFSTEP]
rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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 β
⊢ det (↑(↑(kroneckerMapBilinear f) A) 1 * ↑(↑(kroneckerMapBilinear f) 1) B) =
    det (blockDiagonal fun x => map A fun a => ↑(↑f a) 1) * det (blockDiagonal fun x => map B fun b => ↑(↑f 1) b)
[PROOFSTEP]
rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply, kroneckerMap_diagonal_right _ fun _ => _,
  kroneckerMapBilinear_apply_apply, kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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 β
⊢ ∀ (x : β), ↑(↑f 0) x = 0
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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 β
x✝ : β
⊢ ↑(↑f 0) x✝ = 0
[PROOFSTEP]
exact LinearMap.map_zero₂ _ _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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 β
⊢ ∀ (x : α), ↑(↑f x) 0 = 0
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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 β
x✝ : α
⊢ ↑(↑f x✝) 0 = 0
[PROOFSTEP]
exact map_zero _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : 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 β
⊢ det (blockDiagonal fun x => map A fun a => ↑(↑f a) 1) * det (blockDiagonal fun x => map B fun b => ↑(↑f 1) b) =
    det (map A fun a => ↑(↑f a) 1) ^ Fintype.card n * det (map B fun b => ↑(↑f 1) b) ^ Fintype.card m
[PROOFSTEP]
simp_rw [det_blockDiagonal, Finset.prod_const, Finset.card_univ]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ det (kroneckerMap (fun x x_1 => x * x_1) A B) = det A ^ Fintype.card n * det B ^ Fintype.card m
[PROOFSTEP]
refine' (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ det (map A fun a => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) a) 1) ^ Fintype.card n *
      det (map B fun b => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) 1) b) ^ Fintype.card m =
    det A ^ Fintype.card n * det B ^ Fintype.card m
[PROOFSTEP]
congr 3
[GOAL]
case e_a.e_a.e_M
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (map A fun a => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) a) 1) = A
[PROOFSTEP]
ext i j
[GOAL]
case e_a.e_a.e_M.a.h
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
i j : m
⊢ map A (fun a => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) a) 1) i j = A i j
[PROOFSTEP]
exact mul_one _
[GOAL]
case e_a.e_a.e_M
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (map B fun b => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) 1) b) = B
[PROOFSTEP]
ext i j
[GOAL]
case e_a.e_a.e_M.a.h
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
i j : n
⊢ map B (fun b => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) 1) b) i j = B i j
[PROOFSTEP]
exact one_mul _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
by_cases hA : IsUnit A.det
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
swap
[GOAL]
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case neg.inl
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : IsEmpty n
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
have hAB : ¬IsUnit (A ⊗ₖ B).det := by
  refine' mt (fun hAB => _) hA
  rw [det_kronecker] at hAB 
  exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
⊢ ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
[PROOFSTEP]
refine' mt (fun hAB => _) hA
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
hAB : IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ IsUnit (det A)
[PROOFSTEP]
rw [det_kronecker] at hAB 
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
hAB : IsUnit (det A ^ Fintype.card n * det B ^ Fintype.card m)
⊢ IsUnit (det A)
[PROOFSTEP]
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
hAB : ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
by_cases hB : IsUnit B.det
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
swap
[GOAL]
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
cases isEmpty_or_nonempty m
[GOAL]
case neg.inl
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : IsEmpty m
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
have hAB : ¬IsUnit (A ⊗ₖ B).det := by
  refine' mt (fun hAB => _) hB
  rw [det_kronecker] at hAB 
  exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
⊢ ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
[PROOFSTEP]
refine' mt (fun hAB => _) hB
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
hAB : IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ IsUnit (det B)
[PROOFSTEP]
rw [det_kronecker] at hAB 
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
hAB : IsUnit (det A ^ Fintype.card n * det B ^ Fintype.card m)
⊢ IsUnit (det B)
[PROOFSTEP]
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
hAB : ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
  -- otherwise follows trivially from `mul_kronecker_mul`
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
apply inv_eq_right_inv
[GOAL]
case pos.h
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : IsUnit (det B)
⊢ kroneckerMap (fun x x_1 => x * x_1) A B * kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹ = 1
[PROOFSTEP]
rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ det (kroneckerMap (tmul R) A B) = (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
refine' (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ det (map A fun a => ↑(↑(mk R α β) a) 1) ^ Fintype.card n * det (map B fun b => ↑(↑(mk R α β) 1) b) ^ Fintype.card m =
    (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
simp (config := { eta := false }) only [mk_apply, ← includeLeft_apply (S := R), ← includeRight_apply]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ det (map A fun a => ↑includeLeft a) ^ Fintype.card n * det (map B fun b => ↑includeRight b) ^ Fintype.card m =
    (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ ↑includeLeft (det A) ^ Fintype.card n * ↑includeRight (det B) ^ Fintype.card m =
    (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow, _root_.mul_one, _root_.one_mul]
