α : Type u_1
β : Type ?u.3130
R : Type ?u.3133
n : Type u_2
m : Type ?u.3139
inst✝ : AddGroup α
A : Matrix n n α
ha : IsDiag A
i j : n
h : i ≠ j
⊢ (-A) i j = 0
α : Type u_1
β : Type ?u.3130
R : Type ?u.3133
n : Type u_2
m : Type ?u.3139
inst✝ : AddGroup α
A : Matrix n n α
ha : IsDiag A
⊢ IsDiag (-A)
intro i j h
no goals
α : Type u_1
β : Type ?u.3130
R : Type ?u.3133
n : Type u_2
m : Type ?u.3139
inst✝ : AddGroup α
A : Matrix n n α
ha : IsDiag A
i j : n
h : i ≠ j
⊢ (-A) i j = 0
simp [ha h]