------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties of operations in CancellativeCommutativeSemiring.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (CancellativeCommutativeSemiring)
module Algebra.Properties.CancellativeCommutativeSemiring
{a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
where
open import Algebra.Definitions using (AlmostRightCancellative)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open CancellativeCommutativeSemiring R
open import Algebra.Consequences.Setoid setoid
open import Relation.Binary.Reasoning.Setoid setoid
*-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_
*-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0#
... | yes x≈0 | _ = inj₁ x≈0
... | no _ | yes y≈0 = inj₂ y≈0
... | no x≉0 | no y≉0 = contradiction y≈0 y≉0
where
xy≈x*0 = trans xy≈0 (sym (zeroʳ x))
y≈0 = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0
x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0
... | inj₁ x≈0 = x≉0 x≈0
... | inj₂ y≈0 = y≉0 y≈0
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