α : Type u_1
β : Type ?u.5295
R : Type ?u.5298
n : Type u_2
m : Type ?u.5304
inst✝ : AddZeroClass α
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.5295
R : Type ?u.5298
n : Type u_2
m : Type ?u.5304
inst✝ : AddZeroClass α
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.5295
R : Type ?u.5298
n : Type u_2
m : Type ?u.5304
inst✝ : AddZeroClass α
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]