coeff_one — Mathlib

English

The coefficient of the constant polynomial 1 at index n is 1 if n = 0, and 0 otherwise.

Русский

Коэффициент константного многочлена 1 при индексе n равен 1, если n = 0, и иначе 0.

LaTeX

$$$ \\operatorname{coeff}(1: R[X])(n) = \\begin{cases} 1, & n = 0 \\\\ 0, & n \\neq 0 \\end{cases} $$$

Lean4

theorem coeff_one {n : ℕ} : coeff (1 : R[X]) n = if n = 0 then 1 else 0 :=
  by
  simp_rw [eq_comm (a := n) (b := 0)]
  exact coeff_monomial

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