From 6fce01385c776901c8fb4bba52c520d115f12d7e Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Fri, 8 May 2015 14:00:55 +1000
Subject: [PATCH] feat(library/data/{finset,list}/bigop.lean: generalize bigops
 from group to monoid

---
 library/data/finset/bigop.lean | 6 ++----
 library/data/finset/comb.lean  | 2 +-
 library/data/list/bigop.lean   | 4 ++--
 library/data/list/comb.lean    | 2 +-
 library/data/list/set.lean     | 2 +-
 5 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/library/data/finset/bigop.lean b/library/data/finset/bigop.lean
index ac8f2a8eb..c03814e17 100644
--- a/library/data/finset/bigop.lean
+++ b/library/data/finset/bigop.lean
@@ -1,18 +1,16 @@
 /-
 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
 
-Big operator for finite sets
+Big operator for finite sets.
 -/
 import algebra.group data.finset.basic data.list.bigop
 open algebra finset function binary quot subtype
 
 namespace finset
 variables {A B : Type}
-variable  [g : comm_group B]
+variable  [g : comm_monoid B]
 include g
 
 definition bigop (s : finset A) (f : A → B) : B :=
diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
index 75493175a..7801caba5 100644
--- a/library/data/finset/comb.lean
+++ b/library/data/finset/comb.lean
@@ -153,7 +153,7 @@ variables {A B : Type}
 definition product (s₁ : finset A) (s₂ : finset B) : finset (A × B) :=
 quot.lift_on₂ s₁ s₂
   (λ l₁ l₂,
-    to_finset_of_nodup (list.product (elt_of l₁) (elt_of l₂))
+    to_finset_of_nodup (product (elt_of l₁) (elt_of l₂))
                        (nodup_product (has_property l₁) (has_property l₂)))
   (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_product p₁ p₂))
 
diff --git a/library/data/list/bigop.lean b/library/data/list/bigop.lean
index 89147bbb3..bfb5481fd 100644
--- a/library/data/list/bigop.lean
+++ b/library/data/list/bigop.lean
@@ -12,7 +12,7 @@ open algebra function binary quot
 
 namespace list
 variables {A B : Type}
-variable  [g : group B]
+variable  [g : monoid B]
 include g
 
 definition mulf (f : A → B) : B → A → B :=
@@ -58,7 +58,7 @@ end list
 namespace list
 open perm
 variables {A B : Type}
-variable  [g : comm_group B]
+variable  [g : comm_monoid B]
 include g
 
 theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) :=
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 832ca04fd..322a3d63e 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -268,7 +268,7 @@ theorem zip_unzip : ∀ (l : list (A × B)), zip (pr₁ (unzip l)) (pr₂ (unzip
 definition flat (l : list (list A)) : list A :=
 foldl append nil l
 
-/- cross product -/
+/- product -/
 section product
 
 definition product : list A → list B → list (A × B)
diff --git a/library/data/list/set.lean b/library/data/list/set.lean
index 05174917f..8d9211b7f 100644
--- a/library/data/list/set.lean
+++ b/library/data/list/set.lean
@@ -130,7 +130,7 @@ end erase
 section disjoint
 variable {A : Type}
 
-definition disjoint (l₁ l₂ : list A) : Prop := ∀ a, (a ∈ l₁ → a ∈ l₂ → false)
+definition disjoint (l₁ l₂ : list A) : Prop := ∀ ⦃a⦄, (a ∈ l₁ → a ∈ l₂ → false)
 
 lemma disjoint_left {l₁ l₂ : list A} : disjoint l₁ l₂ → ∀ {a}, a ∈ l₁ → a ∉ l₂ :=
 λ d a, d a