coeffs — Mathlib

English

Define the set of nonzero coefficients of a polynomial as the image of its support under the coefficient map.

Русский

Определим множество ненулевых коэффициентов полинома как образ его опоры по отображению коэффициентов.

LaTeX

$$Let $p$ be a multivariate polynomial. Then $\\operatorname{coeffs}(p) = \\mathrm{Finset}.image (\\lambda m. p.c\\,m) p.\\text{support}$$$

Lean4

/-- The finset of nonzero coefficients of a multivariate polynomial. -/
def coeffs (p : MvPolynomial σ R) : Finset R :=
  letI := Classical.decEq R
  Finset.image p.coeff p.support

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