:: deftheorem defl defines linear FIELD_5:def 1 :
for R being Ring
for p being Polynomial of R holds
( p is linear iff deg p = 1 );