totalDegree — Mathlib

English

totalDegree(p) is the maximum total degree among monomials appearing in p, i.e., the largest sum of exponents across all monomials in p.

Русский

totalDegree(p) есть максимальная общая степень среди мономов, встречающихся в p, то есть наибольшая сумма степеней по всем мономам в p.

LaTeX

$$$\operatorname{totalDegree}(p) = \max_{s \in \operatorname{Supp}(p)} \sum_i s_i$$$

Lean4

/-- `totalDegree p` gives the maximum |s| over the monomials X^s in `p` -/
def totalDegree (p : MvPolynomial σ R) : ℕ :=
  p.support.sup fun s => s.sum fun _ e => e

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