------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of divisibility over commutative magmas
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra using (CommutativeMagma)
module Algebra.Properties.CommutativeMagma.Divisibility
{a ℓ} (CM : CommutativeMagma a ℓ)
where
open import Data.Product.Base using (_×_; _,_)
open CommutativeMagma CM using (magma; _≈_; _∙_; comm)
------------------------------------------------------------------------
-- Re-export the contents of magmas
open import Algebra.Properties.Magma.Divisibility magma public
using (_∣_; _,_)
renaming ( ∣ʳ-respʳ-≈ to ∣-respʳ-≈
; ∣ʳ-respˡ-≈ to ∣-respˡ-≈
; ∣ʳ-resp-≈ to ∣-resp-≈
; x∣ʳyx to x∣yx
; xy≈z⇒y∣ʳz to xy≈z⇒y∣z
)
------------------------------------------------------------------------
-- Further properties
x∣xy : ∀ x y → x ∣ x ∙ y
x∣xy x y = y , comm y x
xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z
xy≈z⇒x∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣xy x y)
x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
x|xy∧y|xy x y = x∣xy x y , x∣yx y x
xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.2
∣-factors = x|xy∧y|xy
{-# WARNING_ON_USAGE ∣-factors
"Warning: ∣-factors was deprecated in v2.2.
Please use x|xy∧y|xy instead. "
#-}
∣-factors-≈ = xy≈z⇒x|z∧y|z
{-# WARNING_ON_USAGE ∣-factors-≈
"Warning: ∣-factors-≈ was deprecated in v2.2.
Please use xy≈z⇒x|z∧y|z instead. "
#-}
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