Multiplication on the rational numbers

Content created by Egbert Rijke, Fredrik Bakke and Julian KG.

Created on 2023-06-25.
Last modified on 2023-09-15.

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

module elementary-number-theory.multiplication-rational-numbers where
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.multiplication-integer-fractions
open import elementary-number-theory.rational-numbers

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


Multiplication on the rational numbers is defined by extending multiplication on integer fractions to the rational numbers.


mul-ℚ :     
mul-ℚ (x , p) (y , q) = in-fraction-ℤ (mul-fraction-ℤ x y)

infixl 40 _*ℚ_
_*ℚ_ = mul-ℚ


Unit laws

left-unit-law-mul-ℚ : (x : )  one-ℚ *ℚ x  x
left-unit-law-mul-ℚ x =
  ( eq-ℚ-sim-fractions-ℤ
    ( mul-fraction-ℤ one-fraction-ℤ (fraction-ℚ x))
    ( fraction-ℚ x)
    ( left-unit-law-mul-fraction-ℤ (fraction-ℚ x))) 
  ( in-fraction-fraction-ℚ x)

right-unit-law-mul-ℚ : (x : )  x *ℚ one-ℚ  x
right-unit-law-mul-ℚ x =
  ( eq-ℚ-sim-fractions-ℤ
    ( mul-fraction-ℤ (fraction-ℚ x) one-fraction-ℤ)
    ( fraction-ℚ x)
    ( right-unit-law-mul-fraction-ℤ (fraction-ℚ x))) 
  ( in-fraction-fraction-ℚ x)

Recent changes