# Relatively prime integers

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Fernando Chu.

Created on 2022-02-17.

module elementary-number-theory.relatively-prime-integers where

Imports
open import elementary-number-theory.absolute-value-integers
open import elementary-number-theory.greatest-common-divisor-integers
open import elementary-number-theory.integers
open import elementary-number-theory.relatively-prime-natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.propositions
open import foundation.universe-levels


## Idea

Two integers are said to be relatively prime if their greatest common divisor is 1.

## Definition

is-relative-prime-ℤ : ℤ → ℤ → UU lzero
is-relative-prime-ℤ x y = is-one-ℤ (gcd-ℤ x y)


## Properties

### Being relatively prime is a proposition

is-prop-is-relative-prime-ℤ : (x y : ℤ) → is-prop (is-relative-prime-ℤ x y)
is-prop-is-relative-prime-ℤ x y = is-set-ℤ (gcd-ℤ x y) one-ℤ


### Two integers are relatively prime if and only if their absolute values are relatively prime natural numbers

is-relatively-prime-abs-is-relatively-prime-ℤ :
{a b : ℤ} → is-relative-prime-ℤ a b →
is-relatively-prime-ℕ (abs-ℤ a) (abs-ℤ b)
is-relatively-prime-abs-is-relatively-prime-ℤ {a} {b} H = is-injective-int-ℕ H

is-relatively-prime-is-relatively-prime-abs-ℤ :
{a b : ℤ} → is-relatively-prime-ℕ (abs-ℤ a) (abs-ℤ b) →
is-relative-prime-ℤ a b
is-relatively-prime-is-relatively-prime-abs-ℤ {a} {b} H = ap int-ℕ H


### For any two integers a and b that are not both 0, the integers a/gcd(a,b) and b/gcd(a,b) are relatively prime

{-
relatively-prime-quotient-div-ℤ :
{a b : ℤ} → (is-nonzero-ℤ a + is-nonzero-ℤ b) →
is-relative-prime-ℤ
( quotient-div-ℤ (gcd-ℤ a b) a (div-left-gcd-ℤ a b))
( quotient-div-ℤ (gcd-ℤ a b) b (div-right-gcd-ℤ a b))
relatively-prime-quotient-div-ℤ H =
is-relatively-prime-is-relatively-prime-abs-ℤ
{!!}
-}