no goals
m : Type ?u.1465983
n : Type u_1
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
R : Type v
inst✝¹ : CommRing R
S : Type w
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
⊢ ↑f (det M) = det (↑(RingHom.mapMatrix f) M)
simp [Matrix.det_apply', f.map_sum, f.map_prod]