constantCoeff_monomial

Mathlib.Algebra.MvPolynomial.Basic

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

← MathLib Explorer

English

For any d, r, the constantCoeff of monomial d r is as above.

Русский

Для любого d, r коэффициента монома описаны выше.

LaTeX

$$$ constantCoeff_monomial (d : Finsupp \\sigma \\mathbb{N}) (r : R) : \\dots $$$

Lean4

theorem constantCoeff_monomial [DecidableEq σ] (d : σ →₀ ℕ) (r : R) :
    constantCoeff (monomial d r) = if d = 0 then r else 0 := by rw [constantCoeff_eq, coeff_monomial]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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