------------------------------------------------------------------------
-- The Agda standard library
--
-- Coprimality
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Integer.Coprimality where
open import Data.Integer.Base using (ℤ; _*_; ∣_∣)
open import Data.Integer.Divisibility using (_∣_)
open import Data.Integer.Properties using (abs-*)
import Data.Nat.Coprimality as ℕ
using (Coprime; sym; coprime?; coprime-divisor)
import Data.Nat.Divisibility as ℕ using (_∣_)
open import Function.Base using (_on_)
open import Level using (0ℓ)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Decidable; Symmetric)
open import Relation.Binary.PropositionalEquality.Core using (subst)
------------------------------------------------------------------------
-- Definition
Coprime : Rel ℤ 0ℓ
Coprime = ℕ.Coprime on ∣_∣
------------------------------------------------------------------------
-- Properties of coprimality
sym : Symmetric Coprime
sym = ℕ.sym
coprime? : Decidable Coprime
coprime? x y = ℕ.coprime? ∣ x ∣ ∣ y ∣
coprime-divisor : ∀ i j k → Coprime i j → i ∣ j * k → i ∣ k
coprime-divisor i j k c eq =
ℕ.coprime-divisor c (subst (∣ i ∣ ℕ.∣_ ) (abs-* j k) eq)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4