:: deftheorem defines X^2+X+1 FIELD_10:def 4 :
X^2+X+1 = <%(1. F_Rat),(1. F_Rat),(1. F_Rat)%>;