Division rings

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

Created on 2022-03-21.
Last modified on 2025-10-31.

module ring-theory.division-rings where
Imports 
open import foundation.cartesian-product-types
open import foundation.negated-equality
open import foundation.universe-levels

open import ring-theory.invertible-elements-rings
open import ring-theory.nontrivial-rings
open import ring-theory.rings

Idea

Division rings are nontrivial rings in which all nonzero elements are invertible.

Definition

is-division-Ring :
  { l : Level} → Ring l → UU l
is-division-Ring R =
  (is-nontrivial-Ring R) ×
  ((x : type-Ring R) → zero-Ring R ≠ x → is-invertible-element-Ring R x)

Recent changes