Division rings

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

Created on 2022-03-21.
Last modified on 2023-03-27.

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

open import ring-theory.invertible-elements-rings
open import ring-theory.rings
open import ring-theory.trivial-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) → ¬ (Id (zero-Ring R) x) → is-invertible-element-Ring R x)

Recent changes