actually add the consequence to CHANGELOG

agda · Jan 24, 2025 · 37c11d5 · 37c11d5
1 parent 74f8275
commit 37c11d5
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -57,6 +57,12 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Consequences.Base`:
+  ```agda
+  integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
+                            NoZeroDivisors _≈_ 0# _•_
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →