@@ -80,7 +80,7 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
8080 total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
8181 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
8282
83−class (VerifiedRing a, Field a) => VerifiedField a where
83+class (VerifiedRingWithUnity a, Field a) => VerifiedField a where
8484 total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
8585 total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity
8686