as_sum_support_C_mul_X_pow — Mathlib · SciLib

English

A polynomial p equals the sum over its support of C(coeff i) X^i, i.e., p = ∑_{i ∈ supp(p)} C(p.coeff i) X^i.

Русский

Полином p равен сумме по опорной поддержке C(coeff i) X^i: p = ∑_{i ∈ supp(p)} C(p.coeff(i)) X^i.

LaTeX

$$$p = \sum_{i \in \operatorname{supp}(p)} C(p.coeff(i)) \cdot X^{i}.$$$

Lean4

theorem as_sum_support_C_mul_X_pow (p : R[X]) : p = ∑ i ∈ p.support, C (p.coeff i) * X ^ i :=
  _root_.trans p.as_sum_support <| by simp only [C_mul_X_pow_eq_monomial]

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