English
The integer degree of a rational function x is defined as the difference between the natDegree of its numerator and the natDegree of its denominator: intDegree(x) = natDegree(x.num) − natDegree(x.denom). In particular intDegree(0) = 0.
Русский
Целочисленная степень рациональной функции x определяется как разность между natDegree его числителя и natDegree его знаменателя: intDegree(x) = natDegree(x.num) − natDegree(x.denom). В частности intDegree(0) = 0.
LaTeX
$$$\\operatorname{intDegree}(x) = \\operatorname{natDegree}(x.num) - \\operatorname{natDegree}(x.denom)$$$
Lean4
/-- `intDegree x` is the degree of the rational function `x`, defined as the difference between
the `natDegree` of its numerator and the `natDegree` of its denominator. In particular,
`intDegree 0 = 0`. -/
def intDegree (x : RatFunc K) : ℤ :=
natDegree x.num - natDegree x.denom
