@@ -123,7 +123,7 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
123||| + Inverse for `<+>`:
123||| + Inverse for `<+>`:
124||| forall a, a <+> inverse a == neutral
124||| forall a, a <+> inverse a == neutral
125||| forall a, inverse a <+> a == neutral
125||| forall a, inverse a <+> a == neutral
126−||| + Associativity of `<*>a:
126+||| + Associativity of `<*>`:
127||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
127||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
128||| + Neutral for `<*>`:
128||| + Neutral for `<*>`:
129||| forall a, a <*> unity == a
129||| forall a, a <*> unity == a