no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
inst✝ : DivisionRing k
f : R →+* k
⊢ leadingCoeff (map f p) = ↑f (leadingCoeff p)
simp only [← coeff_natDegree, coeff_map f, natDegree_map]