@@ -80,7 +80,7 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
80 total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
80 total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
81 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
81 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
83−class (VerifiedRing a, Field a) => VerifiedField a where
83+class (VerifiedRingWithUnity a, Field a) => VerifiedField a where
84 total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
84 total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
85 total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity
85 total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity