This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The ring of rational numbers

{-# OPTIONS --lossy-unification #-}

module elementary-number-theory.ring-of-rational-numbers where

open import commutative-algebra.commutative-rings

open import elementary-number-theory.additive-group-of-rational-numbers
open import elementary-number-theory.multiplication-rational-numbers
open import elementary-number-theory.multiplicative-monoid-of-rational-numbers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.unital-binary-operations
open import foundation.universe-levels

open import group-theory.semigroups

open import ring-theory.rings

Idea

The additive group of rational numbers equipped with multiplication is a commutative division ring.

Definitions

The compatible multiplicative structure on the abelian group of rational numbers

has-mul-abelian-group-add-ℚ : has-mul-Ab abelian-group-add-ℚ
pr1 has-mul-abelian-group-add-ℚ = has-associative-mul-Semigroup semigroup-mul-ℚ
pr1 (pr2 has-mul-abelian-group-add-ℚ) = is-unital-mul-ℚ
pr1 (pr2 (pr2 has-mul-abelian-group-add-ℚ)) = left-distributive-mul-add-ℚ
pr2 (pr2 (pr2 has-mul-abelian-group-add-ℚ)) = right-distributive-mul-add-ℚ

The ring of rational numbers

ring-ℚ : Ring lzero
pr1 ring-ℚ = abelian-group-add-ℚ
pr2 ring-ℚ = has-mul-abelian-group-add-ℚ

Properties

The ring of rational numbers is commutative

commutative-ring-ℚ : Commutative-Ring lzero
pr1 commutative-ring-ℚ = ring-ℚ
pr2 commutative-ring-ℚ = commutative-mul-ℚ