@@ -60,7 +60,6 @@ class Group a => AbelianGroup a where { }
60class AbelianGroup a => Ring a where
60class AbelianGroup a => Ring a where
61 (<.>) : a -> a -> a
61 (<.>) : a -> a -> a
64||| Sets equipped with two binary operations, one associative and commutative
63||| Sets equipped with two binary operations, one associative and commutative
65||| supplied with a neutral element, and the other associative supplied with a
64||| supplied with a neutral element, and the other associative supplied with a
66||| neutral element, with distributivity laws relating the two operations. Must
65||| neutral element, with distributivity laws relating the two operations. Must
@@ -116,6 +115,16 @@ class Ring a => RingWithUnity a where
116class RingWithUnity a => Field a where
115class RingWithUnity a => Field a where
117 inverseM : (x : a) -> Not (x = neutral) -> a
116 inverseM : (x : a) -> Not (x = neutral) -> a
118+sum : (Foldable t, Monoid a) => t a -> a
119+sum = foldr (<+>) neutral
121+product : (Foldable t, RingWithUnity a) => t a -> a
122+product = foldr (<.>) unity
124+power : RingWithUnity a => a -> Nat -> a
126+power x (S n) = x <.> (Algebra.power x n)
120-- XXX todo:
129-- XXX todo:
121-- Structures where "abs" make sense.
130-- Structures where "abs" make sense.