coeff_C — Mathlib

English

The nth coefficient of the constant polynomial C a is a if n = 0 and 0 otherwise.

Русский

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

LaTeX

$$$ \\operatorname{coeff}(\\mathrm{C}\,a)(n) = \\begin{cases} a, & n = 0 \\\\ 0, & n \\neq 0 \\end{cases} $$$

Lean4

theorem coeff_C : coeff (C a) n = ite (n = 0) a 0 :=
  by
  convert coeff_monomial (a := a) (m := n) (n := 0) using 2
  simp [eq_comm]

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