@@ -60,7 +60,6 @@ class Group a => AbelianGroup a where { }
6060class AbelianGroup a => Ring a where
6161 (<.>) : a -> a -> a
6262
63−
6463||| Sets equipped with two binary operations, one associative and commutative
6564||| supplied with a neutral element, and the other associative supplied with a
6665||| neutral element, with distributivity laws relating the two operations. Must
@@ -116,6 +115,16 @@ class Ring a => RingWithUnity a where
116115class RingWithUnity a => Field a where
117116 inverseM : (x : a) -> Not (x = neutral) -> a
118117
118+sum : (Foldable t, Monoid a) => t a -> a
119+sum = foldr (<+>) neutral
120+
121+product : (Foldable t, RingWithUnity a) => t a -> a
122+product = foldr (<.>) unity
123+
124+power : RingWithUnity a => a -> Nat -> a
125+power _ Z = unity
126+power x (S n) = x <.> (Algebra.power x n)
127+
119128
120129-- XXX todo:
121130-- Structures where "abs" make sense.