Multiplication on the rational numbers

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

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

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

module elementary-number-theory.multiplication-rational-numbers where
Imports 
open import elementary-number-theory.addition-integer-fractions
open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.difference-rational-numbers
open import elementary-number-theory.greatest-common-divisor-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integer-fractions
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.interchange-law

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) = rational-fraction-ℤ (mul-fraction-ℤ x y)

mul-ℚ' : ℚ → ℚ → ℚ
mul-ℚ' x y = mul-ℚ y x

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

Properties

The multiplication of a rational number by zero is zero

module _
  (x : ℚ)
  where

  abstract
    left-zero-law-mul-ℚ : zero-ℚ *ℚ x ＝ zero-ℚ
    left-zero-law-mul-ℚ =
      ( eq-ℚ-sim-fraction-ℤ
        ( mul-fraction-ℤ (fraction-ℚ zero-ℚ) (fraction-ℚ x))
        ( fraction-ℚ zero-ℚ)
        ( eq-is-zero-ℤ
          ( ap (mul-ℤ' one-ℤ) (left-zero-law-mul-ℤ (numerator-ℚ x)))
          ( left-zero-law-mul-ℤ _))) ∙
      ( is-retraction-rational-fraction-ℚ zero-ℚ)

    right-zero-law-mul-ℚ : x *ℚ zero-ℚ ＝ zero-ℚ
    right-zero-law-mul-ℚ =
      ( eq-ℚ-sim-fraction-ℤ
        ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ zero-ℚ))
        ( fraction-ℚ zero-ℚ)
        ( eq-is-zero-ℤ
          ( ap (mul-ℤ' one-ℤ) (right-zero-law-mul-ℤ (numerator-ℚ x)))
          ( left-zero-law-mul-ℤ _))) ∙
      ( is-retraction-rational-fraction-ℚ zero-ℚ)

If the product of two rational numbers is zero, the left or right factor is zero

decide-is-zero-factor-is-zero-mul-ℚ :
  (x y : ℚ) → is-zero-ℚ (x *ℚ y) → (is-zero-ℚ x) + (is-zero-ℚ y)
decide-is-zero-factor-is-zero-mul-ℚ x y H =
  rec-coproduct
    ( inl ∘ is-zero-is-zero-numerator-ℚ x)
    ( inr ∘ is-zero-is-zero-numerator-ℚ y)
    ( is-zero-is-zero-mul-ℤ
      ( numerator-ℚ x)
      ( numerator-ℚ y)
      ( ( inv
          ( eq-reduce-numerator-fraction-ℤ
            ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)))) ∙
        ( ap
          ( mul-ℤ'
            ( gcd-ℤ
              ( numerator-ℚ x *ℤ numerator-ℚ y)
              ( denominator-ℚ x *ℤ denominator-ℚ y)))
          ( ( is-zero-numerator-is-zero-ℚ (x *ℚ y) H) ∙
            ( left-zero-law-mul-ℤ
              ( gcd-ℤ
                (numerator-ℚ x *ℤ numerator-ℚ y)
                (denominator-ℚ x *ℤ denominator-ℚ y)))))))

Unit laws for multiplication on rational numbers

abstract
  left-unit-law-mul-ℚ : (x : ℚ) → one-ℚ *ℚ x ＝ x
  left-unit-law-mul-ℚ x =
    ( eq-ℚ-sim-fraction-ℤ
      ( mul-fraction-ℤ one-fraction-ℤ (fraction-ℚ x))
      ( fraction-ℚ x)
      ( left-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙
    ( is-retraction-rational-fraction-ℚ x)

  right-unit-law-mul-ℚ : (x : ℚ) → x *ℚ one-ℚ ＝ x
  right-unit-law-mul-ℚ x =
    ( eq-ℚ-sim-fraction-ℤ
      ( mul-fraction-ℤ (fraction-ℚ x) one-fraction-ℤ)
      ( fraction-ℚ x)
      ( right-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙
    ( is-retraction-rational-fraction-ℚ x)

Multiplication of a rational number by -1 is equal to the negative

abstract
  left-neg-unit-law-mul-ℚ : (x : ℚ) → neg-one-ℚ *ℚ x ＝ neg-ℚ x
  left-neg-unit-law-mul-ℚ x =
    ( eq-ℚ-sim-fraction-ℤ
      ( mul-fraction-ℤ (fraction-ℚ neg-one-ℚ) (fraction-ℚ x))
      ( neg-fraction-ℤ (fraction-ℚ x))
      ( ap-mul-ℤ
        ( left-neg-unit-law-mul-ℤ (numerator-ℚ x))
        ( inv (left-unit-law-mul-ℤ (denominator-ℚ x))))) ∙
    ( is-retraction-rational-fraction-ℚ (neg-ℚ x))

  right-neg-unit-law-mul-ℚ : (x : ℚ) → x *ℚ neg-one-ℚ ＝ neg-ℚ x
  right-neg-unit-law-mul-ℚ x =
    ( eq-ℚ-sim-fraction-ℤ
      ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ neg-one-ℚ))
      ( neg-fraction-ℤ (fraction-ℚ x))
      ( ap-mul-ℤ
        ( right-neg-unit-law-mul-ℤ (numerator-ℚ x))
        ( inv (right-unit-law-mul-ℤ (denominator-ℚ x))))) ∙
    ( is-retraction-rational-fraction-ℚ (neg-ℚ x))

Multiplication of rational numbers is associative

abstract
  associative-mul-ℚ :
    (x y z : ℚ) → (x *ℚ y) *ℚ z ＝ x *ℚ (y *ℚ z)
  associative-mul-ℚ x y z =
    eq-ℚ-sim-fraction-ℤ
      ( mul-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ z))
      ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y *ℚ z)))
      ( transitive-sim-fraction-ℤ
        ( mul-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ z))
        ( mul-fraction-ℤ
          ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
          ( fraction-ℚ z))
        ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y *ℚ z)))
        ( transitive-sim-fraction-ℤ
          ( mul-fraction-ℤ
            ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
            ( fraction-ℚ z))
          ( mul-fraction-ℤ
            ( fraction-ℚ x)
            ( mul-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
          ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y *ℚ z)))
          ( sim-fraction-mul-fraction-ℤ
            ( refl-sim-fraction-ℤ (fraction-ℚ x))
            ( sim-reduced-fraction-ℤ
              ( mul-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))))
          ( associative-mul-fraction-ℤ
            ( fraction-ℚ x)
            ( fraction-ℚ y)
            ( fraction-ℚ z)))
        ( sim-fraction-mul-fraction-ℤ
          ( inv
            ( sim-reduced-fraction-ℤ
              ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))))
          ( refl-sim-fraction-ℤ (fraction-ℚ z))))

Multiplication of rational numbers is commutative

abstract
  commutative-mul-ℚ : (x y : ℚ) → x *ℚ y ＝ y *ℚ x
  commutative-mul-ℚ x y =
    eq-ℚ-sim-fraction-ℤ
      ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
      ( mul-fraction-ℤ (fraction-ℚ y) (fraction-ℚ x))
      ( commutative-mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))

Interchange law for multiplication on rational numbers with itself

abstract
  interchange-law-mul-mul-ℚ :
    (x y u v : ℚ) → (x *ℚ y) *ℚ (u *ℚ v) ＝ (x *ℚ u) *ℚ (y *ℚ v)
  interchange-law-mul-mul-ℚ =
    interchange-law-commutative-and-associative
      mul-ℚ
      commutative-mul-ℚ
      associative-mul-ℚ

Negative laws for multiplication on rational numbers

module _
  (x y : ℚ)
  where

  abstract
    left-negative-law-mul-ℚ : (neg-ℚ x) *ℚ y ＝ neg-ℚ (x *ℚ y)
    left-negative-law-mul-ℚ =
      ( ap ( _*ℚ y) (inv (left-neg-unit-law-mul-ℚ x))) ∙
      ( associative-mul-ℚ neg-one-ℚ x y) ∙
      ( left-neg-unit-law-mul-ℚ (x *ℚ y))

    right-negative-law-mul-ℚ : x *ℚ (neg-ℚ y) ＝ neg-ℚ (x *ℚ y)
    right-negative-law-mul-ℚ =
      ( ap ( x *ℚ_) (inv (right-neg-unit-law-mul-ℚ y))) ∙
      ( inv (associative-mul-ℚ x y neg-one-ℚ)) ∙
      ( right-neg-unit-law-mul-ℚ (x *ℚ y))

abstract
  negative-law-mul-ℚ : (x y : ℚ) → (neg-ℚ x) *ℚ (neg-ℚ y) ＝ x *ℚ y
  negative-law-mul-ℚ x y =
    ( left-negative-law-mul-ℚ x (neg-ℚ y)) ∙
    ( ap neg-ℚ (right-negative-law-mul-ℚ x y)) ∙
    ( neg-neg-ℚ (x *ℚ y))

  swap-neg-mul-ℚ : (x y : ℚ) → x *ℚ (neg-ℚ y) ＝ (neg-ℚ x) *ℚ y
  swap-neg-mul-ℚ x y =
    ( right-negative-law-mul-ℚ x y) ∙
    ( inv (left-negative-law-mul-ℚ x y))

Multiplication on rational numbers distributes over addition

abstract
  left-distributive-mul-add-ℚ :
    (x y z : ℚ) → x *ℚ (y +ℚ z) ＝ (x *ℚ y) +ℚ (x *ℚ z)
  left-distributive-mul-add-ℚ x y z =
    eq-ℚ-sim-fraction-ℤ
      ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z)))
      ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z)))
      ( transitive-sim-fraction-ℤ
        ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z)))
        ( mul-fraction-ℤ
          ( fraction-ℚ x)
          ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
        ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z)))
        ( transitive-sim-fraction-ℤ
          ( mul-fraction-ℤ
            ( fraction-ℚ x)
            ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
          ( add-fraction-ℤ
            ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
            ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z)))
          ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z)))
          ( sim-fraction-add-fraction-ℤ
            ( sim-reduced-fraction-ℤ
              ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)))
            ( sim-reduced-fraction-ℤ
              ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z))))
          ( left-distributive-mul-add-fraction-ℤ
            ( fraction-ℚ x)
            ( fraction-ℚ y)
            ( fraction-ℚ z)))
        ( sim-fraction-mul-fraction-ℤ
          ( refl-sim-fraction-ℤ (fraction-ℚ x))
          ( transitive-sim-fraction-ℤ
            ( fraction-ℚ (y +ℚ z))
            ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
            ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))
            ( symmetric-sim-fraction-ℤ
              ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))
              ( reduce-fraction-ℤ
                ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
              ( sim-reduced-fraction-ℤ
                (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))))
            ( refl-sim-fraction-ℤ (fraction-ℚ (y +ℚ z))))))

  right-distributive-mul-add-ℚ :
    (x y z : ℚ) → (x +ℚ y) *ℚ z ＝ (x *ℚ z) +ℚ (y *ℚ z)
  right-distributive-mul-add-ℚ x y z =
    ( commutative-mul-ℚ (x +ℚ y) z) ∙
    ( left-distributive-mul-add-ℚ z x y) ∙
    ( ap-add-ℚ (commutative-mul-ℚ z x) (commutative-mul-ℚ z y))

Multiplication on rational numbers distributes over the difference

abstract
  left-distributive-mul-diff-ℚ :
    (z x y : ℚ) → z *ℚ (x -ℚ y) ＝ (z *ℚ x) -ℚ (z *ℚ y)
  left-distributive-mul-diff-ℚ z x y =
    ( left-distributive-mul-add-ℚ z x (neg-ℚ y)) ∙
    ( ap ((z *ℚ x) +ℚ_) (right-negative-law-mul-ℚ z y))

  right-distributive-mul-diff-ℚ :
    (x y z : ℚ) → (x -ℚ y) *ℚ z ＝ (x *ℚ z) -ℚ (y *ℚ z)
  right-distributive-mul-diff-ℚ x y z =
    ( right-distributive-mul-add-ℚ x (neg-ℚ y) z) ∙
    ( ap ((x *ℚ z) +ℚ_) (left-negative-law-mul-ℚ y z))

See also

Recent changes