------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of divisibility over semigroups
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Semigroup)
module Algebra.Properties.Semigroup.Divisibility
{a ℓ} (S : Semigroup a ℓ) where
open import Data.Product.Base using (_,_)
open import Relation.Binary.Definitions using (Transitive)
open Semigroup S
------------------------------------------------------------------------
-- Re-export magma divisibility
open import Algebra.Properties.Magma.Divisibility magma public
------------------------------------------------------------------------
-- Properties of _∣ʳ_
x∣ʳy⇒x∣ʳzy : ∀ {x y} z → x ∣ʳ y → x ∣ʳ z ∙ y
x∣ʳy⇒x∣ʳzy z (p , px≈y) = z ∙ p , trans (assoc z p _) (∙-congˡ px≈y)
x∣ʳy⇒xz∣ʳyz : ∀ {x y} z → x ∣ʳ y → x ∙ z ∣ʳ y ∙ z
x∣ʳy⇒xz∣ʳyz z (p , px≈y) = p , trans (sym (assoc p _ z)) (∙-congʳ px≈y)
∣ʳ-trans : Transitive _∣ʳ_
∣ʳ-trans (p , px≈y) (q , qy≈z) =
q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z)
------------------------------------------------------------------------
-- Properties of _∣ˡ__
x∣ˡy⇒x∣ˡyz : ∀ {x y} z → x ∣ˡ y → x ∣ˡ y ∙ z
x∣ˡy⇒x∣ˡyz z (p , xp≈y) = p ∙ z , trans (sym (assoc _ p z)) (∙-congʳ xp≈y)
x∣ˡy⇒zx∣ˡzy : ∀ {x y} z → x ∣ˡ y → z ∙ x ∣ˡ z ∙ y
x∣ˡy⇒zx∣ˡzy z (p , xp≈y) = p , trans (assoc z _ p) (∙-congˡ xp≈y)
∣ˡ-trans : Transitive _∣ˡ_
∣ˡ-trans (p , xp≈y) (q , yq≈z) =
p ∙ q , trans (sym (assoc _ p q)) (trans (∙-congʳ xp≈y) yq≈z)
------------------------------------------------------------------------
-- Properties of _∥_
∥-trans : Transitive _∥_
∥-trans (x∣y , y∣x) (y∣z , z∣y) = ∣ʳ-trans x∣y y∣z , ∣ʳ-trans z∣y y∣x
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.3
∣∣-trans = ∥-trans
{-# WARNING_ON_USAGE ∣∣-trans
"Warning: ∣∣-trans was deprecated in v2.3.
Please use ∥-trans instead. "
#-}
∣-trans = ∣ʳ-trans
{-# WARNING_ON_USAGE ∣-trans
"Warning: ∣-trans was deprecated in v2.3.
Please use ∣ʳ-trans 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