------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of divisibility over semirings
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Semiring)
module Algebra.Properties.Semiring.Divisibility
{a ℓ} (R : Semiring a ℓ) where
open Semiring R
------------------------------------------------------------------------
-- Re-exporting divisibility over monoids
open import Algebra.Properties.Monoid.Divisibility *-monoid public
renaming (ε∣_ to 1∣_)
------------------------------------------------------------------------
-- Divisibility properties specific to semirings.
infixr 8 _∣0
_∣0 : ∀ x → x ∣ 0#
x ∣0 = 0# , zeroˡ x
0∣x⇒x≈0 : ∀ {x} → 0# ∣ x → x ≈ 0#
0∣x⇒x≈0 (q , q*0≈x) = trans (sym q*0≈x) (zeroʳ q)
x∣y∧y≉0⇒x≉0 : ∀ {x y} → x ∣ y → y ≉ 0# → x ≉ 0#
x∣y∧y≉0⇒x≉0 x∣y y≉0 x≈0 = y≉0 (0∣x⇒x≈0 (∣-respˡ x≈0 x∣y))
0∤1 : 0# ≉ 1# → 0# ∤ 1#
0∤1 0≉1 0∣1 = 0≉1 (sym (0∣x⇒x≈0 0∣1))
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