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
p : R[X]
⊢ Monic (map f p) ↔ Monic p
rw [Monic, leadingCoeff_map, ← f.map_one, Function.Injective.eq_iff f.injective, Monic]