Discrete fields

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-04-22.
Last modified on 2023-05-04.

module commutative-algebra.discrete-fields where
open import commutative-algebra.commutative-rings

open import foundation.universe-levels

open import ring-theory.division-rings


A discrete field is a commutative division ring. They are called discrete, because only nonzero elements are assumed to be invertible.


is-discrete-field-Commutative-Ring : {l : Level}  Commutative-Ring l  UU l
is-discrete-field-Commutative-Ring A =
  is-division-Ring (ring-Commutative-Ring A)

Recent changes