fixed name clash

agda · MatthewDaggitt · Feb 5, 2024 · Feb 2, 2024 · Feb 2, 2024 · Feb 2, 2024
commit 98e8363141d138c43807dd2104ac078b6fe6481d
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -97,7 +97,7 @@ Additions to existing modules
 
 * In `Algebra.Properties.Semiring.Mult`:
   ```agda
-  ×-homo-0 : ∀ x → 0 × x ≈ 0# * x
+  ×-homo-0# : ∀ x → 0 × x ≈ 0# * x
   ```
 
 * In `Data.Fin.Properties`:

diff --git a/src/Algebra/Properties/Semiring/Mult.agda b/src/Algebra/Properties/Semiring/Mult.agda
@@ -36,8 +36,8 @@ open import Algebra.Properties.Monoid.Mult +-monoid public
 
 -- (0 ×_) is (0# *_)
 
-×-homo-0 : ∀ x → 0 × x ≈ 0# * x
-×-homo-0 x = sym (zeroˡ x)
+×-homo-0# : ∀ x → 0 × x ≈ 0# * x
+×-homo-0# x = sym (zeroˡ x)
 
 -- (n ×_) commutes with _*_