support_integralNormalization_subset

English

The support of integralNormalization(p) is contained in the support of p.

Русский

Поддержка интегральной нормализации содержится в поддержке p.

LaTeX

$$$\operatorname{supp}(\operatorname{integralNormalization}(p)) \subseteq \operatorname{supp}(p)$$$

Lean4

theorem support_integralNormalization_subset : (integralNormalization p).support ⊆ p.support :=
  by
  intro
  simp +contextual [sum_def, integralNormalization, coeff_monomial, mem_support_iff]

Похожие утверждения