as_sum_range — Mathlib

English

A polynomial p equals the sum over i in range(natDegree(p)+1) of monomial i (coeff p i).

Русский

Полином p равен сумме по i в range(natDegree(p)+1) мономиона i с коэффициентом coeff p i.

LaTeX

$$$p = \sum_{i \in \operatorname{range}(\operatorname{natDegree}(p) + 1)} \operatorname{monomial}(i, \operatorname{coeff}(p, i)).$$$

Lean4

theorem as_sum_range (p : R[X]) : p = ∑ i ∈ range (p.natDegree + 1), monomial i (coeff p i) :=
  p.as_sum_range' _ (lt_add_one _)

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