as_sum_range' — Mathlib

English

For p and n with natDegree(p) < n, p equals the finite sum over range(n) of monomial i times coeff p i.

Русский

Для p и n с natDegree(p) < n, p равен сумме по диапазону range(n) мономиона i на coeff p i.

LaTeX

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

Lean4

theorem as_sum_range' (p : R[X]) (n : ℕ) (hn : p.natDegree < n) : p = ∑ i ∈ range n, monomial i (coeff p i) :=
  p.sum_monomial_eq.symm.trans <| p.sum_over_range' monomial_zero_right _ hn

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