English
The supremum degree of a single basis element δ_a with coefficient r is either ⊥ if r=0, or D(a) if r≠0.
Русский
Для базисного элемента δ_a с коэффициентом r верхняя грань степени равна ⊥, если r=0; иначе равна D(a).
LaTeX
$$$\\supDegree D (\\text{single } a r) = \\begin{cases} \\bot, & r=0 \\\\ D(a), & r\\neq 0 \\end{cases}$$$
Lean4
/-- Let `R` be a semiring, let `A` be an `AddZeroClass`, let `B` be an `OrderBot`,
and let `D : A → B` be a "degree" function.
For an element `f : R[A]`, the element `supDegree f : B` is the supremum of all the elements in the
support of `f`, or `⊥` if `f` is zero.
Often, the Type `B` is `WithBot A`,
If, further, `A` has a linear order, then this notion coincides with the usual one,
using the maximum of the exponents.
If `A := σ →₀ ℕ` then `R[A] = MvPolynomial σ R`, and if we equip `σ` with a linear order then
the induced linear order on `Lex A` equips `MvPolynomial` ring with a
[monomial order](https://en.wikipedia.org/wiki/Monomial_order) (i.e. a linear order on `A`, the
type of (monic) monomials in `R[A]`, that respects addition). We make use of this monomial order
by taking `D := toLex`, and different monomial orders could be accessed via different type
synonyms once they are added. -/
abbrev supDegree (f : R[A]) : B :=
f.support.sup D
