no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : degree f ≠ ↑i
⊢ coeff (integralNormalization f) i = coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
rw [integralNormalization_coeff, if_neg hi]