:: deftheorem defines degree RATFUNC1:def 18 :
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being rational_function of L holds degree z = max ((degree ((NF z) `1)),(degree ((NF z) `2)));