Field
From Groupprops
Definition
A field is a set (that we'll call ) equipped with the following:
- An (infix) binary operation
, called the addition
- An (infix) binary operation
, called the multiplication
- Two distinct constants
, called zero and one
- A unary operation denoted by the prefix symbol
(called the negative, or additive inverse)
- A map
such that the following compatibility conditions hold:
-
forms an abelian group with binary operation
, inverse map
, and identity element
. This is called the additive group of
.
-
gives an associative binary operation on
- The following distributivity law holds:
-
forms an abelian group with binary operation
, inverse map
and identity element
. This is called the multiplicative group of
.