A field has two operations, the addition and the multiplication.
It is an abelian group under addition, with 0 as additive identity.
The nonzero elements form an abelian group under multiplication,
and the multiplication is distributive over addition.
In order to avoid existential quantifiers, fields can be defined by two binary operations
(addition and multiplication),
two unary operations (yielding the additive and multiplicative inverses, respectively),
and two nullary operations (the constants 0 and 1).
