as_sum_support — Mathlib · SciLib

English

A polynomial p equals the sum over its support of monomials with the corresponding coefficients, i.e., p = ∑_{i ∈ supp(p)} monomial(i, p.coeff(i)).

Русский

Полином p равен сумме по опорной поддержке мономиалов с соответствующими коэффициентами: p = ∑_{i ∈ supp(p)} monomial(i, p.coeff(i)).

LaTeX

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

Lean4

theorem as_sum_support (p : R[X]) : p = ∑ i ∈ p.support, monomial i (p.coeff i) :=
  (sum_monomial_eq p).symm

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