for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds
p1,p2 have_common_roots