feat(library/data/finset): add bigop for finset + commutative groups

library/data/finset/basic.lean

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 
 Finite sets
 -/
-import data.nat data.list.perm data.subtype algebra.binary algebra.function logic.identities
+import data.nat data.list.perm data.subtype algebra.binary
 open nat quot list subtype binary function
 open [declarations] perm
 

library/data/finset/bigop.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.finset
+Author: Leonardo de Moura
+
+Finite sets big operators
+-/
+import algebra.group data.finset.basic
+open algebra finset function binary quot
+
+namespace finset
+variables {A B : Type}
+variable  [g : comm_group B]
+include g
+
+protected definition mulf (f : A → B) : B → A → B :=
+λ b a, b * f a
+
+protected theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) :=
+right_commutative_compose_right (@has_mul.mul B g) f (@mul.right_comm B g)
+
+definition bigop (s : finset A) (f : A → B) : B :=
+acc (mulf f) (mulf_rcomm f) 1 s
+end finset

library/data/finset/default.lean

@@ -7,4 +7,4 @@ Author: Leonardo de Moura
 
 Finite sets
 -/
-import data.finset.basic
+import data.finset.basic data.finset.bigop