lcoeff_apply — Mathlib

English

For any commutative semiring R, any natural number n, and any polynomial f in R[X], the nth left-coefficient and the ordinary nth coefficient agree: lcoeff R n f = coeff f n.

Русский

Для любой полумной системы R, натурального числа n и многочлена f в R[X] коэффициент на степень n, получаемый функцией lcoeff, совпадает с обычным коэффициентом на n: lcoeff R n f = coeff f n.

LaTeX

$$$\mathrm{lcoeff}_R(n,f) = \mathrm{coeff}(f,n)$$$

Lean4

@[simp]
theorem lcoeff_apply (n : ℕ) (f : R[X]) : lcoeff R n f = coeff f n :=
  rfl

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