support_integralNormalization — Mathlib

English

The support of integralNormalization(f) equals the support of f for a semiring with no zero divisors.

Русский

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

LaTeX

$$$\operatorname{support}(\operatorname{integralNormalization}(f)) = \operatorname{support}(f)$$$

Lean4

@[simp]
theorem support_integralNormalization {f : R[X]} : (integralNormalization f).support = f.support :=
  by
  nontriviality R using Subsingleton.eq_zero
  have : IsDomain R := { }
  by_cases hf : f = 0; · simp [hf]
  ext i
  refine ⟨fun h => support_integralNormalization_subset h, ?_⟩
  simp only [integralNormalization_coeff, mem_support_iff]
  intro hfi
  split_ifs with hi <;> simp [hf, hfi]

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