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
- 2023-03-27. Fernando Chu. Change integral domains definition (#545).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).