coeff_one — Mathlib

English

Let σ be a type and R a semiring. For every index n, the coefficient of the constant unit series at n is 1 if n is the zero index and 0 otherwise.

Русский

Пусть σ — тип, R — полугруппа. Для любого индекса n коэффициент единичного константного ряда равен 1, если n — нулевой индекс, и 0 в противном случае.

LaTeX

$$$\\operatorname{coeff}_{n}(1 : MvPowerSeries\\ σ \\; R) = \\begin{cases}1, & n = 0 \\\\ 0, & \\text{otherwise} \\end{cases}$$$

Lean4

theorem coeff_one [DecidableEq σ] : coeff n (1 : MvPowerSeries σ R) = if n = 0 then 1 else 0 :=
  coeff_monomial _ _ _

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