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

Idea

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

Definition

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

• 2023-05-04. Egbert Rijke. Cleaning up commutative algebra (#589).
• 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
• 2023-03-10. Fredrik Bakke. Additions to fix-import (#497).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
• 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).