vars — Mathlib

English

For any p, the set of variables appearing in p equals the finite set of indices with nonzero degree, i.e., vars(p) = degrees(p) toFinset.

Русский

Для любого p множество переменных p совпадает с конечным множеством индексов с ненулевой степенью; то есть vars(p) = degrees(p) toFinset.

LaTeX

$$$$ \mathrm{vars}(p) = (\mathrm{degrees}(p))^{\mathrm{toFinset}} $$$$

Lean4

/-- `vars p` is the set of variables appearing in the polynomial `p` -/
def vars (p : MvPolynomial σ R) : Finset σ :=
  letI := Classical.decEq σ
  p.degrees.toFinset

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