Multiplication on integer fractions

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

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

module elementary-number-theory.multiplication-integer-fractions where
Imports 
open import elementary-number-theory.addition-integer-fractions
open import elementary-number-theory.addition-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.multiplication-positive-and-negative-integers
open import elementary-number-theory.positive-integers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.identity-types
open import foundation.subtypes

Idea

Multiplication on integer fractions is an extension of the multiplicative operation on the integers to integer fractions. Note that the basic properties of multiplication on integer fraction only hold up to fraction similarity.

Definition

mul-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ
pr1 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos)) =
  m *ℤ m'
pr1 (pr2 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
  n *ℤ n'
pr2 (pr2 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
  is-positive-mul-ℤ n-pos n'-pos

mul-fraction-ℤ' : fraction-ℤ → fraction-ℤ → fraction-ℤ
mul-fraction-ℤ' x y = mul-fraction-ℤ y x

infixl 40 _*fraction-ℤ_
_*fraction-ℤ_ = mul-fraction-ℤ

ap-mul-fraction-ℤ :
  {x y x' y' : fraction-ℤ} → x ＝ x' → y ＝ y' →
  x *fraction-ℤ y ＝ x' *fraction-ℤ y'
ap-mul-fraction-ℤ p q = ap-binary mul-fraction-ℤ p q

Properties

Multiplication on integer fractions respects the similarity relation

sim-fraction-mul-fraction-ℤ :
  {x x' y y' : fraction-ℤ} →
  sim-fraction-ℤ x x' →
  sim-fraction-ℤ y y' →
  sim-fraction-ℤ (x *fraction-ℤ y) (x' *fraction-ℤ y')
sim-fraction-mul-fraction-ℤ
  {(nx , dx , dxp)} {(nx' , dx' , dx'p)}
  {(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q =
  equational-reasoning
    (nx *ℤ ny) *ℤ (dx' *ℤ dy')
    ＝ (nx *ℤ dx') *ℤ (ny *ℤ dy')
      by interchange-law-mul-mul-ℤ nx ny dx' dy'
    ＝ (nx' *ℤ dx) *ℤ (ny' *ℤ dy)
      by ap-mul-ℤ p q
    ＝ (nx' *ℤ ny') *ℤ (dx *ℤ dy)
      by interchange-law-mul-mul-ℤ nx' dx ny' dy

Unit laws for multiplication on integer fractions

left-unit-law-mul-fraction-ℤ :
  (k : fraction-ℤ) →
  sim-fraction-ℤ (mul-fraction-ℤ one-fraction-ℤ k) k
left-unit-law-mul-fraction-ℤ k = refl

right-unit-law-mul-fraction-ℤ :
  (k : fraction-ℤ) →
  sim-fraction-ℤ (mul-fraction-ℤ k one-fraction-ℤ) k
right-unit-law-mul-fraction-ℤ (n , d , p) =
  ap-mul-ℤ (right-unit-law-mul-ℤ n) (inv (right-unit-law-mul-ℤ d))

Multiplication on integer fractions is associative

associative-mul-fraction-ℤ :
  (x y z : fraction-ℤ) →
  sim-fraction-ℤ
    (mul-fraction-ℤ (mul-fraction-ℤ x y) z)
    (mul-fraction-ℤ x (mul-fraction-ℤ y z))
associative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) =
  ap-mul-ℤ (associative-mul-ℤ nx ny nz) (inv (associative-mul-ℤ dx dy dz))

Multiplication on integer fractions is commutative

commutative-mul-fraction-ℤ :
  (x y : fraction-ℤ) → sim-fraction-ℤ (x *fraction-ℤ y) (y *fraction-ℤ x)
commutative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) =
  ap-mul-ℤ (commutative-mul-ℤ nx ny) (commutative-mul-ℤ dy dx)

Multiplication on integer fractions distributes on the left over addition

left-distributive-mul-add-fraction-ℤ :
  (x y z : fraction-ℤ) →
  sim-fraction-ℤ
    (mul-fraction-ℤ x (add-fraction-ℤ y z))
    (add-fraction-ℤ (mul-fraction-ℤ x y) (mul-fraction-ℤ x z))
left-distributive-mul-add-fraction-ℤ
  (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) =
    ( ap
      ( ( nx *ℤ (ny *ℤ dz +ℤ nz *ℤ dy)) *ℤ_)
      ( ( interchange-law-mul-mul-ℤ dx dy dx dz) ∙
        ( associative-mul-ℤ dx dx (dy *ℤ dz)))) ∙
    ( interchange-law-mul-mul-ℤ
      ( nx)
      ( ny *ℤ dz +ℤ nz *ℤ dy)
      ( dx)
      ( dx *ℤ (dy *ℤ dz))) ∙
    ( inv
      ( associative-mul-ℤ
        ( nx *ℤ dx)
        ( ny *ℤ dz +ℤ nz *ℤ dy)
        ( dx *ℤ (dy *ℤ dz)))) ∙
    ( ap
      ( _*ℤ (dx *ℤ (dy *ℤ dz)))
      ( ( left-distributive-mul-add-ℤ
          ( nx *ℤ dx)
          ( ny *ℤ dz)
          ( nz *ℤ dy)) ∙
        ( ap-add-ℤ
          ( interchange-law-mul-mul-ℤ nx dx ny dz))
          ( interchange-law-mul-mul-ℤ nx dx nz dy)))

The inclusion of integers preserves multiplication

abstract
  mul-in-fraction-ℤ :
    (x y : ℤ) →
    in-fraction-ℤ x *fraction-ℤ in-fraction-ℤ y ＝ in-fraction-ℤ (x *ℤ y)
  mul-in-fraction-ℤ x y =
    eq-pair
      ( ap-mul-ℤ (left-unit-law-mul-ℤ x) (left-unit-law-mul-ℤ y))
      ( eq-type-subtype subtype-positive-ℤ refl)

Recent changes