coeffs_eq_empty_of_subsingleton — Mathlib

English

If the coefficient ring R is a subsingleton, then every multivariate polynomial p over R has no nonzero coefficients; equivalently p.coeffs = ∅ for all p.

Русский

Пусть R — одноэлементный тип. Тогда любой многочлен MvPolynomial σ R имеет пустой набор ненулевых коэффициентов: p.coeffs = ∅ для любого p.

LaTeX

$$$ [\\text{Subsingleton } R] \\Rightarrow \\forall p : \\mathrm{MvPolynomial}(\\sigma, R), p.\\mathrm{coeffs} = \\emptyset. $$$

Lean4

@[nontriviality]
theorem coeffs_eq_empty_of_subsingleton [Subsingleton R] (p : MvPolynomial σ R) : p.coeffs = ∅ := by
  simpa [coeffs] using Subsingleton.eq_zero p

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