α : Type u_1
β : Type ?u.6998
R : Type ?u.7001
n : Type u_2
m : Type ?u.7007
inst✝ : AddGroup α
A B : Matrix n n α
ha : IsDiag A
hb : IsDiag B
i j : n
h : i ≠ j
⊢ (A - B) i j = 0
α : Type u_1
β : Type ?u.6998
R : Type ?u.7001
n : Type u_2
m : Type ?u.7007
inst✝ : AddGroup α
A B : Matrix n n α
ha : IsDiag A
hb : IsDiag B
⊢ IsDiag (A - B)
intro i j h
no goals
α : Type u_1
β : Type ?u.6998
R : Type ?u.7001
n : Type u_2
m : Type ?u.7007
inst✝ : AddGroup α
A B : Matrix n n α
ha : IsDiag A
hb : IsDiag B
i j : n
h : i ≠ j
⊢ (A - B) i j = 0
simp [ha h, hb h]