The field of rational numbers

Content created by Fredrik Bakke and malarbol.

Created on 2024-04-25.
Last modified on 2024-04-25.

module elementary-number-theory.field-of-rational-numbers where
Imports 
open import commutative-algebra.discrete-fields

open import elementary-number-theory.multiplicative-group-of-rational-numbers
open import elementary-number-theory.nonzero-rational-numbers
open import elementary-number-theory.ring-of-rational-numbers

open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types

open import ring-theory.division-rings

Idea

The type of rational numbers equipped with addition and multiplication is a discrete field, i.e., a commutative ring whose nonzero elements are invertible.

Definitions

The ring of rational numbers is a division ring

is-division-ring-ℚ : is-division-Ring ring-ℚ
pr1 is-division-ring-ℚ = is-nonzero-one-ℚ ∘ inv
pr2 is-division-ring-ℚ x H = is-invertible-element-ring-is-nonzero-ℚ x (H ∘ inv)

The rational numbers form a discrete field

is-discrete-field-ℚ : is-discrete-field-Commutative-Ring commutative-ring-ℚ
is-discrete-field-ℚ = is-division-ring-ℚ

Recent changes