-- Mathlib/Data/Matrix/Kronecker.lean
theorem det_kronecker [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R]
    (A : Matrix m m R) (B : Matrix n n R) :
    det (A ⊗ₖ B) = det A ^ Fintype.card n * det B ^ Fintype.card m

Proof state:
R : Type u_1
m : Type u_9
n : Type u_10
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 x1 x2 => x1 * x2) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
refine (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_

Result:
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ (A.map fun a => ((Algebra.lmul ℕ R).toLinearMap a) 1).det ^ Fintype.card n *
      (B.map fun b => ((Algebra.lmul ℕ R).toLinearMap 1) b).det ^ Fintype.card m =
    A.det ^ Fintype.card n * B.det ^ Fintype.card m

Proof state:
case e_a.e_a.e_M
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ (B.map fun b => ((Algebra.lmul ℕ R).toLinearMap 1) b) = B

Tactic:
ext i j

Result:
case e_a.e_a.e_M.a
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ B.map (fun b => ((Algebra.lmul ℕ R).toLinearMap 1) b) i j = B i j

Proof state:
case e_a.e_a.e_M.a
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ A.map (fun a => ((Algebra.lmul ℕ R).toLinearMap a) 1) i j = A i j

Tactic:
exact mul_one _

Result:
no goals

Proof state:
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ (A.map fun a => ((Algebra.lmul ℕ R).toLinearMap a) 1).det ^ Fintype.card n *
      (B.map fun b => ((Algebra.lmul ℕ R).toLinearMap 1) b).det ^ Fintype.card m =
    A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
congr 3

Result:
case e_a.e_a.e_M
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ (A.map fun a => ((Algebra.lmul ℕ R).toLinearMap a) 1) = A

case e_a.e_a.e_M
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ (B.map fun b => ((Algebra.lmul ℕ R).toLinearMap 1) b) = B

Proof state:
case e_a.e_a.e_M
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ (A.map fun a => ((Algebra.lmul ℕ R).toLinearMap a) 1) = A

Tactic:
ext i j

Result:
case e_a.e_a.e_M.a
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ A.map (fun a => ((Algebra.lmul ℕ R).toLinearMap a) 1) i j = A i j

Proof state:
case e_a.e_a.e_M.a
R : Type u_1
m : Type u_9
n : Type u_10
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
⊢ B.map (fun b => ((Algebra.lmul ℕ R).toLinearMap 1) b) i j = B i j

Tactic:
exact one_mul _

Result:
no goals