coeffs — Mathlib

English

The coeffs of a polynomial p form a finite set consisting of the nonzero coefficients, obtained by applying the coefficient extraction to the support of p.

Русский

Коэффициенты многочлена образуют конечное множество ненулевых коэффициентов, получаемых применением коэффициентной выборки к опоре p.

LaTeX

$$$\\text{coeffs}(p) = \\mathrm{Finset}.image (\\lambda n. p.\\text{coeff } n)\\; p.\\text{support}$$$

Lean4

/-- The finset of nonzero coefficients of a polynomial. -/
def coeffs (p : R[X]) : Finset R :=
  letI := Classical.decEq R
  Finset.image (fun n => p.coeff n) p.support

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