:: deftheorem defines square-free FIELD_14:def 3 :
for R being non degenerated comRing
for p being Polynomial of R holds
( p is square-free iff p is_square-free_over R );