for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr st R is Noetherian holds
for n being Nat holds Polynom-Ring (n,R) is Noetherian