add: definitions and one consequence

CHANGELOG.md

@@ -85,3 +85,10 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
+* In `Algebra.Definitions`:
+  ```agda
+  NoZeroDivisors : A → Op₂ A → Set _
+  Integral       : A → A → Op₂ A → Set _
+  ```
+  (see [discussion on issue #2554](https://github.com/agda/agda-stdlib/issues/2554))

src/Algebra/Consequences/Base.agda

@@ -15,6 +15,7 @@ open import Algebra.Definitions
 open import Data.Sum.Base
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
 
@@ -28,6 +29,14 @@ module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
                                      Involutive _≈_ f
   reflexive∧selfInverse⇒involutive refl inv _ = inv refl
 
+module _ {ℓ} {_•_ : Op₂ A} {0# 1# : A} (_≈_ : Rel A ℓ) where
+
+  integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
+                            NoZeroDivisors _≈_ 0# _•_
+  integral⇒noZeroDivisors (inj₁ 1#≈0#)          = contradiction 1#≈0#
+  integral⇒noZeroDivisors (inj₂ noZeroDivisors) = λ _ → noZeroDivisors
+
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Algebra/Definitions.agda

@@ -66,6 +66,12 @@ RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
 Zero : A → Op₂ A → Set _
 Zero z ∙ = (LeftZero z ∙) × (RightZero z ∙)
 
+NoZeroDivisors : A → Op₂ A → Set _
+NoZeroDivisors z _∙_ = ∀ {x y} → (x ∙ y) ≈ z → x ≈ z ⊎ y ≈ z
+
+Integral : A → A → Op₂ A → Set _
+Integral 1# 0# _∙_ = 1# ≈ 0# ⊎ NoZeroDivisors 0# _∙_
+
 LeftInverse : A → Op₁ A → Op₂ A → Set _
 LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) ≈ e