:: deftheorem defines Leading-Coefficient FIELD_11:def 2 :
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Leading-Coefficient p = p . (Leading-Term p);