R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
a✝ : ℕ
⊢ a✝ ∈ support (integralNormalization f) → a✝ ∈ support f
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
⊢ support (integralNormalization f) ⊆ support f
intro
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
a✝ : ℕ
⊢ a✝ ∈ support (integralNormalization f) → a✝ ∈ support f
simp (config := { contextual := true }) [integralNormalization, coeff_monomial, mem_support_iff]