:: deftheorem defines X^3-1 FIELD_10:def 2 :
X^3-1 = ((0_. F_Rat) +* (0,(- 1))) +* (3,1);