@@ -106,7 +106,7 @@ class AbelianGroup a => Ring a where
106class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
106class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
107 total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
107 total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
108 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
108 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
109− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
109+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)
111||| Sets equipped with two binary operations, one associative and commutative
111||| Sets equipped with two binary operations, one associative and commutative
112||| supplied with a neutral element, and the other associative supplied with a
112||| supplied with a neutral element, and the other associative supplied with a