English
The infDegree of a polynomial in the AddMonoidAlgebra is the infimum (minimum in a linear order) of the degrees of the nonzero terms in its support.
Русский
infDegree степенного типа — это наименьшее по порядку значение степеней в поддержке ненулевых членов.
LaTeX
$$$$\operatorname{infDegree}(f) = \inf\{ D(a) : a \in \mathrm{supp}(f)\}.$$$$
Lean4
/-- Let `R` be a semiring, let `A` be an `AddZeroClass`, let `T` be an `OrderTop`,
and let `D : A → T` be a "degree" function.
For an element `f : R[A]`, the element `infDegree f : T` is the infimum of all the elements in the
support of `f`, or `⊤` if `f` is zero.
Often, the Type `T` is `WithTop A`,
If, further, `A` has a linear order, then this notion coincides with the usual one,
using the minimum of the exponents. -/
abbrev infDegree (f : R[A]) : T :=
f.support.inf D
