totalDegree_eq — Mathlib

English

The total degree of p equals the maximum over the support of p of the sum of the exponents, equivalently the maximum cardinality of the exponents represented.

Русский

Общая степень p равна максимуму по опорe p суммы степеней, эквивалентно максимуму по конкатенации степеней.

LaTeX

$$$\operatorname{totalDegree}(p) = \max_{s \in \operatorname{Supp}(p)} \left|\mathrm{toMultiset}(s)\right| = \max_{s \in \operatorname{Supp}(p)} \sum_i s_i$$$

Lean4

theorem totalDegree_eq (p : MvPolynomial σ R) : p.totalDegree = p.support.sup fun m => Multiset.card (toMultiset m) :=
  by
  rw [totalDegree]
  congr; funext m
  exact (Finsupp.card_toMultiset _).symm

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