support — Mathlib

English

The support of a polynomial expressed via finsupp coincides with the support of its finsupp representation.

Русский

Поддержка полинома через представление finsupp совпадает с поддержкой самого представления finsupp.

LaTeX

$$$\operatorname{support}(\langle p \rangle) = p.\operatorname{support}$$$

Lean4

/-- The set of all `n` such that `X^n` has a non-zero coefficient. -/
def support : R[X] → Finset ℕ
  | ⟨p⟩ => p.support

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