Library
▹
Algebra
▹
Fields
Definition 2.9.1.
We define:
Fld
:
=
{
rings
R
:
R
is commutative
and
R
×
=
(
R
) ∖ {0
R
}
}
We write “let
F
be a field” for “let
F
∈
Fld
.”
References.
https://en.wikipedia.org/wiki/Field_(mathematics)
https://mathworld.wolfram.com/Field.html
https://proofwiki.org/wiki/Definition:Field_(Abstract_Algebra)
https://ncatlab.org/nlab/show/field
https://coq.inria.fr/library/Coq.setoid_ring.Field_theory.html#field_theory
https://leanprover-community.github.io/mathlib_docs/algebra/field.html#field