theorem :: FIELD_14:34

for R being non degenerated comRing
for p being Polynomial of R holds
( p is square-free iff for q being non constant Polynomial of R holds not q `^ 2 divides p ) by lemsq;