:: deftheorem defines is_reduced_wrt GROEB_1:def 7 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) holds
( P is_reduced_wrt T iff for p being Polynomial of n,L st p in P holds
( p is_monic_wrt T & p is_irreducible_wrt P \ {p},T ) );