no goals
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (powerBasis hf).gen = f * ↑C (Polynomial.leadingCoeff f)⁻¹
rw [powerBasis_gen, minpoly_root hf]