case mk.mk
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
h : (a, b) ≠ (c, d)
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
⊢ IsDiag (kroneckerMap (fun x x_1 => x * x_1) A B)
rintro ⟨a, b⟩ ⟨c, d⟩ h
case mk.mk
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
case mk.mk
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
h : (a, b) ≠ (c, d)
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
simp only [Prod.mk.inj_iff, Ne.def, not_and_or] at h
case mk.mk.inl
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
hac : ¬a = c
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0

case mk.mk.inr
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
hbd : ¬b = d
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
case mk.mk
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
cases' h with hac hbd
no goals
case mk.mk.inl
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
hac : ¬a = c
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
simp [hA hac]
no goals
case mk.mk.inr
α : Type u_1
β : Type ?u.20075
R : Type ?u.20078
n : Type u_3
m : Type u_2
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
hbd : ¬b = d
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
simp [hB hbd]