case pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
by_cases hA : IsUnit A.det
case neg
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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 pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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 pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
swap
case pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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 pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
by_cases hB : IsUnit B.det
case neg
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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 pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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 pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
swap
case neg.inl
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹

case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
case neg
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
cases isEmpty_or_nonempty n
case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
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)
no goals
case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
no goals
case neg.inl
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
exact Subsingleton.elim _ _
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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))
refine' mt (fun hAB => _) hA
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
rw [det_kronecker] at hAB
no goals
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
case neg.inl
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹

case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
case neg
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
cases isEmpty_or_nonempty m
case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
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)
no goals
case neg.inr
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
no goals
case neg.inl
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
exact Subsingleton.elim _ _
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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))
refine' mt (fun hAB => _) hB
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
rw [det_kronecker] at hAB
no goals
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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)
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
case pos.h
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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
case pos
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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⁻¹
apply inv_eq_right_inv
no goals
case pos.h
R : Type u_3
α : Type ?u.173346
α' : Type ?u.173349
β : Type ?u.173352
β' : Type ?u.173355
γ : Type ?u.173358
γ' : Type ?u.173361
l : Type ?u.173364
m : Type u_1
n : Type u_2
p : Type ?u.173373
q : Type ?u.173376
r : Type ?u.173379
l' : Type ?u.173382
m' : Type ?u.173385
n' : Type ?u.173388
p' : Type ?u.173391
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
rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]