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