coeffs_one — Mathlib

English

Let R be a semiring. The only nonzero coefficient of the constant polynomial 1 is 1; hence the coefficients appearing in 1 are contained in {1}.

Русский

Пусть R — полукольцо. Единичный константный многочлен имеет единственный ненулевой коэффициент, равный 1; следовательно, все коэффициенты 1 принадлежат множеству коэффициентов этого многочлена.

LaTeX

$$$\operatorname{coeffs}(1) \subseteq \{1\}$$$

Lean4

theorem coeffs_one : coeffs (1 : R[X]) ⊆ { 1 } := by
  classical
  simp_rw [coeffs, Finset.image_subset_iff]
  simp_all [coeff_one]

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