:: deftheorem defines is_square-free_over FIELD_14:def 2 :
for R, S being non degenerated comRing
for p being Polynomial of R holds
( p is_square-free_over S iff for q1 being non constant Polynomial of S
for q2 being Polynomial of S holds
( not q2 = p or not q1 `^ 2 divides q2 ) );