coeffs_one_of_nontrivial — Mathlib

English

If R is nontrivial, the coefficient set of the constant polynomial 1 is the singleton {1}.

Русский

Если R не тривиален, набор коэффициентов константного полинома 1 равен {1}.

LaTeX

$$$ [\\text{Nontrivial } R] \\Rightarrow coeffs(1 : \\mathrm{MvPolynomial}(\\sigma, R)) = \\{1\\}. $$$

Lean4

@[simp]
theorem coeffs_one_of_nontrivial [Nontrivial R] : coeffs (1 : MvPolynomial σ R) = { 1 } :=
  by
  apply Finset.Subset.antisymm coeffs_one
  simp only [coeffs, Finset.singleton_subset_iff, Finset.mem_image]
  exact ⟨0, by simp⟩

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