on master help sign in
Fix documentation for distributivity of rings

Rings have a distributivity law between `<.>` and `<+>` not between `<.>` and `<->`

commit95fe866302a82f9cc14d18d707a5c66347698cbf authoruwap <me@uwap.name> dateThu 30 Jul 2015, 02:35 (11 years ago) parentbc4b485
1 file changed+3−3
libs/contrib/Control/Algebra.idr+3−3
libs/contrib/Control/Algebra.idr+3−3
@@ -54,7 +54,7 @@ class Group a => AbelianGroup a where { }
5454||| forall a, inverse a <+> a == neutral
5555||| + Associativity of `<.>`:
5656||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
57−||| + Distributivity of `<.>` and `<->`:
57+||| + Distributivity of `<.>` and `<+>`:
5858||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
5959||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
6060class AbelianGroup a => Ring a where
@@ -80,7 +80,7 @@ class AbelianGroup a => Ring a where
8080||| + Neutral for `<.>`:
8181||| forall a, a <.> unity == a
8282||| forall a, unity <.> a == a
83−||| + Distributivity of `<.>` and `<->`:
83+||| + Distributivity of `<.>` and `<+>`:
8484||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
8585||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
8686class Ring a => RingWithUnity a where
@@ -109,7 +109,7 @@ class Ring a => RingWithUnity a where
109109||| + InverseM of `<.>`, except for neutral
110110||| forall a /= neutral, a <.> inverseM a == unity
111111||| forall a /= neutral, inverseM a <.> a == unity
112−||| + Distributivity of `<.>` and `<->`:
112+||| + Distributivity of `<.>` and `<+>`:
113113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
114114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
115115class RingWithUnity a => Field a where