:: deftheorem defLT defines Leading-Term FIELD_11:def 1 :
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( ( p <> 0_ (n,R) implies Leading-Term p = (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) ) & ( not p <> 0_ (n,R) implies Leading-Term p = EmptyBag n ) );