ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Fix documentation for distributivity of rings

Browse Source 
Rings have a distributivity law between `<.>` and `<+>` not between `<.>` and `<->`
This commit is contained in:
uwap 2015-07-30 02:35:59 +02:00
parent bc4b4852e7
commit 95fe866302
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/contrib/Control/Algebra.idr
View File

@ -54,7 +54,7 @@ class Group a => AbelianGroup a where { }
||| forall a, inverse a <+> a == neutral
||| + Associativity of `<.>`:
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Distributivity of `<.>` and `<->`:
||| + Distributivity of `<.>` and `<+>`:
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class AbelianGroup a => Ring a where
@ -80,7 +80,7 @@ class AbelianGroup a => Ring a where
||| + Neutral for `<.>`:
||| forall a, a <.> unity == a
||| forall a, unity <.> a == a
||| + Distributivity of `<.>` and `<->`:
||| + Distributivity of `<.>` and `<+>`:
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class Ring a => RingWithUnity a where
@ -109,7 +109,7 @@ class Ring a => RingWithUnity a where
||| + InverseM of `<.>`, except for neutral
||| forall a /= neutral, a <.> inverseM a == unity
||| forall a /= neutral, inverseM a <.> a == unity
||| + Distributivity of `<.>` and `<->`:
||| + Distributivity of `<.>` and `<+>`:
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class RingWithUnity a => Field a where