# Multiplicative inverses of positive integer fractions

Content created by Fredrik Bakke and malarbol.

Created on 2024-04-25.

module elementary-number-theory.multiplicative-inverses-positive-integer-fractions where

Imports
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.positive-integer-fractions
open import elementary-number-theory.reduced-integer-fractions

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.transport-along-identifications


## Idea

The integer fraction obtained by swapping the numerator and the denominator of a positive integer fraction is a multiplicative inverse of the original fraction up to the canonical similarity relation on integer fractions: its multiplication with the original fraction is similar to one.

## Definitions

### The inverse of a positive integer fraction

module _
(x : fraction-ℤ) (H : is-positive-fraction-ℤ x)
where

inv-is-positive-fraction-ℤ : fraction-ℤ
pr1 inv-is-positive-fraction-ℤ = denominator-fraction-ℤ x
pr1 (pr2 inv-is-positive-fraction-ℤ) = numerator-fraction-ℤ x
pr2 (pr2 inv-is-positive-fraction-ℤ) = H


## Properties

### The inverse of a positive reduced integer fraction is reduced

module _
(x : fraction-ℤ) (P : is-positive-fraction-ℤ x)
where

is-reduced-inv-is-positive-fraction-ℤ :
is-reduced-fraction-ℤ x →
is-reduced-fraction-ℤ (inv-is-positive-fraction-ℤ x P)
is-reduced-inv-is-positive-fraction-ℤ =
inv-tr
( is-one-ℤ)
( is-commutative-gcd-ℤ
( denominator-fraction-ℤ x)
( numerator-fraction-ℤ x))


### The multiplication of a positive integer fraction with its inverse is similar to one

module _
(x : fraction-ℤ) (P : is-positive-fraction-ℤ x)
where

left-inverse-law-mul-is-positive-fraction-ℤ :
sim-fraction-ℤ
(mul-fraction-ℤ (inv-is-positive-fraction-ℤ x P) x)
(one-fraction-ℤ)
left-inverse-law-mul-is-positive-fraction-ℤ =
( right-unit-law-mul-ℤ _) ∙
( commutative-mul-ℤ
( denominator-fraction-ℤ x)
( numerator-fraction-ℤ x)) ∙
( inv (left-unit-law-mul-ℤ _))

right-inverse-law-mul-is-positive-fraction-ℤ :
sim-fraction-ℤ
(mul-fraction-ℤ x (inv-is-positive-fraction-ℤ x P))
(one-fraction-ℤ)
right-inverse-law-mul-is-positive-fraction-ℤ =
( right-unit-law-mul-ℤ _) ∙
( commutative-mul-ℤ
( numerator-fraction-ℤ x)
( denominator-fraction-ℤ x)) ∙
( inv (left-unit-law-mul-ℤ _))