α : Type u_1
β : Type u_2
R : Type ?u.2825
n : Type u_3
m : Type ?u.2831
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : IsDiag A
f : α → β
hf : f 0 = 0
i j : n
h : i ≠ j
⊢ Matrix.map A f i j = 0
α : Type u_1
β : Type u_2
R : Type ?u.2825
n : Type u_3
m : Type ?u.2831
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : IsDiag A
f : α → β
hf : f 0 = 0
⊢ IsDiag (Matrix.map A f)
intro i j h
no goals
α : Type u_1
β : Type u_2
R : Type ?u.2825
n : Type u_3
m : Type ?u.2831
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : IsDiag A
f : α → β
hf : f 0 = 0
i j : n
h : i ≠ j
⊢ Matrix.map A f i j = 0
simp [ha h, hf]