no goals
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : Monic f
hf' : optParam (f ≠ 0) (_ : f ≠ 0)
⊢ minpoly K (powerBasis hf').gen = f
rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]