as_sum_range_C_mul_X_pow' — Mathlib

English

For p and n with natDegree(p) < n, p equals the sum over range(n) of C(coeff p i) X^i.

Русский

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

LaTeX

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

Lean4

theorem as_sum_range_C_mul_X_pow' (p : R[X]) {n : ℕ} (hn : p.natDegree < n) :
    p = ∑ i ∈ range n, C (coeff p i) * X ^ i :=
  (p.as_sum_range' _ hn).trans <| by simp only [C_mul_X_pow_eq_monomial]

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