α : Type u_2
β : Type ?u.8104
R : Type u_1
n : Type u_3
m : Type ?u.8113
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : IsDiag A
i j : n
h : i ≠ j
⊢ (k • A) i j = 0
α : Type u_2
β : Type ?u.8104
R : Type u_1
n : Type u_3
m : Type ?u.8113
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : IsDiag A
⊢ IsDiag (k • A)
intro i j h
no goals
α : Type u_2
β : Type ?u.8104
R : Type u_1
n : Type u_3
m : Type ?u.8113
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : IsDiag A
i j : n
h : i ≠ j
⊢ (k • A) i j = 0
simp [ha h]