Remove zero arguments for IsNonAssociativeRing

lexvanderstoep · lexvanderstoep · commit 23b7da7c5645 · 2024-06-16T20:16:37.000+02:00
Now that we've replaced the field `zero` with a definition, we
need to update the usages of `IsNonAssociativeRing`.
diff --git 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

Original file line number	Diff line number	Diff line change
`@@ -347,8 +347,6 @@ nonAssociativeRing R S = record`
`347`	`347`	`; -identity = UnitalMagma.identity (unitalMagma R.-unitalMagma S.*-unitalMagma)`
`348`	`348`	`; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <> x <> y <*> z)`
`349`	`349`	`, (λ x y z → (R.distribʳ , S.distribʳ) <> x <> y <*> z)`
`350`		`- ; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)`
`351`		`- , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)`
`352`	`350`	`}`
`353`	`351`
`354`	`352`	`} where module R = NonAssociativeRing R; module S = NonAssociativeRing S`