R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
this : coeff f i = 0 → degree f ≠ ↑i
⊢ coeff (integralNormalization f) i = if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ coeff (integralNormalization f) i = if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
have : f.coeff i = 0 → f.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
this : coeff f i = 0 → degree f ≠ ↑i
⊢ coeff (integralNormalization f) i = if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
simp (config := { contextual := true }) [integralNormalization, coeff_monomial, this,
  mem_support_iff]