vars_monomial — Mathlib

English

For a nonzero coefficient r, the variables of monomial(s,r) equal the support of s.

Русский

Для ненулевого коэффициента r переменные монома monomial(s,r) равны поддержке s.

LaTeX

$$$$ \mathrm{vars}(\mathrm{monomial}(s,r)) = \mathrm{support}(s) $$$$

Lean4

@[simp]
theorem vars_monomial (h : r ≠ 0) : (monomial s r).vars = s.support := by
  classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

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