:: deftheorem defines X^2+X+1 FIELD_9:def 15 :
X^2+X+1 = <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;