coeffs_one

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.coeffs_one

English

The coefficient set of the constant polynomial 1 is contained in {1}.

Русский

Множество коэффициентов константного полинома 1 содержится в {1}.

LaTeX

$$coeffs(1) ⊆ {1}$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru