Library ▹ Algebra ▹ Fields
Definition 2.9.1.  We define:
Fld := {rings R : R is commutative and R× = (R) ∖ {0R}}
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
[View Source]