zero_notMem_coeffs — Mathlib

English

The zero coefficient does not appear in the coefficient set of any polynomial.

Русский

Нулевой коэффициент не входит в множество коэффициентов любого полинома.

LaTeX

$$$ 0 \\notin p.\\mathrm{coeffs} $ for all p : \\mathrm{MvPolynomial}(\\sigma, R). $$$

Lean4

theorem zero_notMem_coeffs (p : MvPolynomial σ R) : 0 ∉ p.coeffs :=
  by
  intro hz
  obtain ⟨n, hnsupp, hn⟩ := mem_coeffs_iff.mp hz
  exact (mem_support_iff.mp hnsupp) hn.symm

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