From a223b9b1f7b4e6dd857f62b644c3d3f4e1048700 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Apr 2015 19:59:26 -0700
Subject: [PATCH] feat(library/data/finset): add bigop for finset + commutative
 groups

---
 library/data/finset/basic.lean   |  2 +-
 library/data/finset/bigop.lean   | 26 ++++++++++++++++++++++++++
 library/data/finset/default.lean |  2 +-
 3 files changed, 28 insertions(+), 2 deletions(-)
 create mode 100644 library/data/finset/bigop.lean

diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index 1b2a09d2e..c215324ef 100644
--- a/library/data/finset/basic.lean
+++ b/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
 
diff --git a/library/data/finset/bigop.lean b/library/data/finset/bigop.lean
new file mode 100644
index 000000000..565ccf97e
--- /dev/null
+++ b/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
diff --git a/library/data/finset/default.lean b/library/data/finset/default.lean
index 8f1d99146..34546d346 100644
--- a/library/data/finset/default.lean
+++ b/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