R : Type u_5
α : Type u_3
α' : Type ?u.341956
β : Type u_4
β' : Type ?u.341962
γ : Type ?u.341965
γ' : Type ?u.341968
l : Type ?u.341971
m : Type u_1
n : Type u_2
p : Type ?u.341980
q : Type ?u.341983
r : Type ?u.341986
l' : Type ?u.341989
m' : Type ?u.341992
n' : Type ?u.341995
p' : Type ?u.341998
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)
R : Type u_5
α : Type u_3
α' : Type ?u.341956
β : Type u_4
β' : Type ?u.341962
γ : Type ?u.341965
γ' : Type ?u.341968
l : Type ?u.341971
m : Type u_1
n : Type u_2
p : Type ?u.341980
q : Type ?u.341983
r : Type ?u.341986
l' : Type ?u.341989
m' : Type ?u.341992
n' : Type ?u.341995
p' : Type ?u.341998
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)
refine' (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans _
R : Type u_5
α : Type u_3
α' : Type ?u.341956
β : Type u_4
β' : Type ?u.341962
γ : Type ?u.341965
γ' : Type ?u.341968
l : Type ?u.341971
m : Type u_1
n : Type u_2
p : Type ?u.341980
q : Type ?u.341983
r : Type ?u.341986
l' : Type ?u.341989
m' : Type ?u.341992
n' : Type ?u.341995
p' : Type ?u.341998
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)
R : Type u_5
α : Type u_3
α' : Type ?u.341956
β : Type u_4
β' : Type ?u.341962
γ : Type ?u.341965
γ' : Type ?u.341968
l : Type ?u.341971
m : Type u_1
n : Type u_2
p : Type ?u.341980
q : Type ?u.341983
r : Type ?u.341986
l' : Type ?u.341989
m' : Type ?u.341992
n' : Type ?u.341995
p' : Type ?u.341998
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)
simp (config := { eta := false }) only [mk_apply, ← includeLeft_apply, ← includeRight_apply]
R : Type u_5
α : Type u_3
α' : Type ?u.341956
β : Type u_4
β' : Type ?u.341962
γ : Type ?u.341965
γ' : Type ?u.341968
l : Type ?u.341971
m : Type u_1
n : Type u_2
p : Type ?u.341980
q : Type ?u.341983
r : Type ?u.341986
l' : Type ?u.341989
m' : Type ?u.341992
n' : Type ?u.341995
p' : Type ?u.341998
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)
R : Type u_5
α : Type u_3
α' : Type ?u.341956
β : Type u_4
β' : Type ?u.341962
γ : Type ?u.341965
γ' : Type ?u.341968
l : Type ?u.341971
m : Type u_1
n : Type u_2
p : Type ?u.341980
q : Type ?u.341983
r : Type ?u.341986
l' : Type ?u.341989
m' : Type ?u.341992
n' : Type ?u.341995
p' : Type ?u.341998
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)
simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
no goals
R : Type u_5
α : Type u_3
α' : Type ?u.341956
β : Type u_4
β' : Type ?u.341962
γ : Type ?u.341965
γ' : Type ?u.341968
l : Type ?u.341971
m : Type u_1
n : Type u_2
p : Type ?u.341980
q : Type ?u.341983
r : Type ?u.341986
l' : Type ?u.341989
m' : Type ?u.341992
n' : Type ?u.341995
p' : Type ?u.341998
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)
simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow,
  _root_.mul_one, _root_.one_mul]