coeff_monomial — Mathlib

English

If the index type σ is empty, every polynomial equals a constant C of its constant term: p = C(p.coeff 0).

Русский

Если множество индексов пусто, любой полином равен константе C от своего константного коэффициента: p = C(p.coeff 0).

LaTeX

$$$[IsEmpty\;\sigma]\ (p)\;:\ p = C(p.coeff\ 0\ p)$$$

Lean4

@[simp]
theorem coeff_monomial [DecidableEq σ] (m n) (a) : coeff m (monomial n a : MvPolynomial σ R) = if n = m then a else 0 :=
  Finsupp.single_apply

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