:: deftheorem Def3 defines degree HILB10_5:def 3 :
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b₄ being Nat holds
( ( p <> 0_ (n,L) implies ( b₄ = degree p iff ( ex s being bag of n st
( s in Support p & b₄ = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b₄ ) ) ) ) & ( not p <> 0_ (n,L) implies ( b₄ = degree p iff b₄ = 0 ) ) );