no goals
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pnz : p ≠ 0
hp : ↑(Polynomial.aeval x) p = 0
⊢ ↑(Polynomial.aeval x) (p * ↑C (leadingCoeff p)⁻¹) = 0
simp [hp]