mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-11 22:58:40 +00:00
30 lines
664 B
Agda
30 lines
664 B
Agda
{-# OPTIONS --safe --warning=error #-}
|
||
|
||
open import LogicalFormulae
|
||
open import Naturals
|
||
open import Integers
|
||
open import Groups
|
||
open import Rings
|
||
open import Fields
|
||
open import PrimeNumbers
|
||
open import Setoids
|
||
open import Functions
|
||
open import FieldOfFractions
|
||
|
||
module Rationals where
|
||
|
||
ℚ : Set
|
||
ℚ = fieldOfFractionsSet ℤIntDom
|
||
|
||
_+Q_ : ℚ → ℚ → ℚ
|
||
a +Q b = fieldOfFractionsPlus ℤIntDom a b
|
||
|
||
_*Q_ : ℚ → ℚ → ℚ
|
||
a *Q b = fieldOfFractionsTimes ℤIntDom a b
|
||
|
||
ℚRing : Ring (fieldOfFractionsSetoid ℤIntDom) _+Q_ _*Q_
|
||
ℚRing = fieldOfFractionsRing ℤIntDom
|
||
|
||
ℚField : Field ℚRing
|
||
ℚField = fieldOfFractions ℤIntDom
|