diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3c1c689d57..ac6de1fb81 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,6 +15,8 @@ Bug-fixes
   These operators are used for equational reasoning of heterogeneous equality
   `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
   `x` and `y` to have the same type, making them unusable in most situations.
+* Removed unnecessary parameter `zero : Zero 0# *` from
+  `Algebra.Structures.IsNonAssociativeRing`.
 
 Non-backwards compatible changes
 --------------------------------
diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda
index 3c0ec699ee..867de0c5fb 100644
--- a/src/Algebra/Construct/DirectProduct.agda
+++ b/src/Algebra/Construct/DirectProduct.agda
@@ -347,8 +347,6 @@ nonAssociativeRing R S = record
       ; *-identity       = UnitalMagma.identity (unitalMagma R.*-unitalMagma S.*-unitalMagma)
       ; distrib          = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
                             , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
-      ; zero             = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)
-                            , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)
       }
 
   } where module R = NonAssociativeRing R; module S = NonAssociativeRing S
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 1aae80d1cc..4f74515f06 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -805,7 +805,6 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a
     *-cong           : Congruent₂ *
     *-identity       : Identity 1# *
     distrib          : * DistributesOver +
-    zero             : Zero 0# *
 
   open IsAbelianGroup +-isAbelianGroup public
     renaming
@@ -833,18 +832,21 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a
     ; isGroup                 to +-isGroup
     )
 
-  zeroˡ : LeftZero 0# *
-  zeroˡ = proj₁ zero
-
-  zeroʳ : RightZero 0# *
-  zeroʳ = proj₂ zero
-
   distribˡ : * DistributesOverˡ +
   distribˡ = proj₁ distrib
 
   distribʳ : * DistributesOverʳ +
   distribʳ = proj₂ distrib
 
+  zeroˡ : LeftZero 0# *
+  zeroˡ = Consequences.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ setoid +-cong *-cong +-assoc distribʳ +-identityʳ -‿inverseʳ
+
+  zeroʳ : RightZero 0# *
+  zeroʳ = Consequences.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ setoid +-cong *-cong +-assoc distribˡ +-identityʳ -‿inverseʳ
+
+  zero : Zero 0# *
+  zero = zeroˡ , zeroʳ
+
   *-isMagma : IsMagma *
   *-isMagma = record
     { isEquivalence = isEquivalence