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
Imports 
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

Idea

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

Definition

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

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

Properties

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