:: deftheorem Def6 defines is_monic_wrt GROEB_1:def 6 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty multLoopStr_0
for p being Polynomial of n,L holds
( p is_monic_wrt T iff HC (p,T) = 1. L );