diff --git a/algebra/big_operators.lean b/algebra/big_operators.lean
index 9189d31752072..4ac1818eff8be 100644
--- a/algebra/big_operators.lean
+++ b/algebra/big_operators.lean
@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 Some big operators for lists and finite sets.
 -/
 import data.list.basic data.list.perm data.finset
-  algebra.group algebra.ordered_group algebra.group_power
+import algebra.group algebra.ordered_group algebra.group_power
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -304,6 +304,11 @@ finset.strong_induction_on s
         ← insert_erase (mem_erase.2 ⟨h₂ x hx hx1, h₃ x hx⟩),
         prod_insert (not_mem_erase _ _), ih', mul_one, h₁ x hx])
 
+@[to_additive finset.sum_eq_zero]
+lemma prod_eq_one [comm_monoid β] {f : α → β} {s : finset α} (h : ∀x∈s, f x = 1) : s.prod f = 1 :=
+calc s.prod f = s.prod (λx, 1) : finset.prod_congr rfl h
+  ... = 1 : finset.prod_const_one
+
 end comm_monoid
 
 lemma sum_smul [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
@@ -355,6 +360,14 @@ finset.induction_on s (by simp)
     ... ≤ (insert a s).sum (λ a, card (t a)) :
     by rw sum_insert has; exact add_le_add_left ih _)
 
+lemma gsmul_sum [add_comm_group β] {f : α → β} {s : finset α} (z : ℤ) :
+  gsmul z (s.sum f) = s.sum (λa, gsmul z (f a)) :=
+begin
+  refine (finset.sum_hom (gsmul z) _ _).symm,
+  exact gsmul_zero _,
+  assume x y, exact gsmul_add _ _ _
+end
+
 end finset
 
 namespace finset
@@ -523,6 +536,7 @@ section group
 open list
 variables [group α] [group β]
 
+@[to_additive is_add_group_hom.sum]
 theorem is_group_hom.prod (f : α → β) [is_group_hom f] (l : list α) :
   f (prod l) = prod (map f l) :=
 by induction l; simp only [*, is_group_hom.mul f, is_group_hom.one f, prod_nil, prod_cons, map]
@@ -537,6 +551,26 @@ theorem inv_prod : ∀ l : list α, (prod l)⁻¹ = prod (map (λ x, x⁻¹) (re
 
 end group
 
+section comm_group
+variables [comm_group α] [comm_group β] (f : α → β) [is_group_hom f]
+
+@[to_additive is_add_group_hom.multiset_sum]
+lemma is_group_hom.multiset_prod (m : multiset α) : f m.prod = (m.map f).prod :=
+quotient.induction_on m $ assume l, by simp [is_group_hom.prod f l]
+
+@[to_additive is_add_group_hom.finset_sum]
+lemma is_group_hom.finset_prod (g : γ → α) (s : finset γ) : f (s.prod g) = s.prod (f ∘ g) :=
+show f (s.val.map g).prod = (s.val.map (f ∘ g)).prod, by rw [is_group_hom.multiset_prod f]; simp
+
+end comm_group
+
+@[to_additive is_add_group_hom_finset_sum]
+lemma is_group_hom_finset_prod {α β γ} [group α] [comm_group β] (s : finset γ)
+  (f : γ → α → β) [∀c, is_group_hom (f c)] : is_group_hom (λa, s.prod (λc, f c a)) :=
+⟨assume a b, by simp only [λc, is_group_hom.mul (f c), finset.prod_mul_distrib]⟩
+
+attribute [instance] is_group_hom_finset_prod is_add_group_hom_finset_sum
+
 namespace multiset
 variables [decidable_eq α]
 
diff --git a/algebra/group.lean b/algebra/group.lean
index 790c98b66d8ef..e16ef6efa3b2d 100644
--- a/algebra/group.lean
+++ b/algebra/group.lean
@@ -667,6 +667,21 @@ protected lemma is_conj (f : α → β) [is_group_hom f] {a b : α} : is_conj a
 
 end is_group_hom
 
+@[to_additive is_add_group_hom_add]
+lemma is_group_hom_mul {α β} [group α] [comm_group β]
+  (f g : α → β) [is_group_hom f] [is_group_hom g] :
+  is_group_hom (λa, f a * g a) :=
+⟨assume a b, by simp only [is_group_hom.mul f, is_group_hom.mul g, mul_comm, mul_assoc, mul_left_comm]⟩
+
+attribute [instance] is_group_hom_mul is_add_group_hom_add
+
+@[to_additive is_add_group_hom_neg]
+lemma is_group_hom_inv {α β} [group α] [comm_group β] (f : α → β) [is_group_hom f] :
+  is_group_hom (λa, (f a)⁻¹) :=
+⟨assume a b, by rw [is_group_hom.mul f, mul_inv]⟩
+
+attribute [instance] is_group_hom_inv is_add_group_hom_neg
+
 /-- Predicate for group anti-homomorphism, or a homomorphism
   into the opposite group. -/
 class is_group_anti_hom {β : Type*} [group α] [group β] (f : α → β) : Prop :=
@@ -697,6 +712,13 @@ calc f (a - b) = f (a + -b)   : rfl
 
 end is_add_group_hom
 
+lemma is_add_group_hom_sub {α β} [add_group α] [add_comm_group β]
+  (f g : α → β) [is_add_group_hom f] [is_add_group_hom g] :
+  is_add_group_hom (λa, f a - g a) :=
+is_add_group_hom_add f (λa, - g a)
+
+attribute [instance] is_add_group_hom_sub
+
 namespace units
 variables [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
 
diff --git a/algebra/group_power.lean b/algebra/group_power.lean
index c7a92fcba11d4..f266e95c9c0e7 100644
--- a/algebra/group_power.lean
+++ b/algebra/group_power.lean
@@ -11,7 +11,8 @@ a^n is used for the first, but users can locally redefine it to gpow when needed
 
 Note: power adopts the convention that 0^0=1.
 -/
-import algebra.char_zero data.int.basic algebra.group algebra.ordered_field data.list.basic
+import algebra.char_zero algebra.group algebra.ordered_field
+import data.int.basic data.list.basic
 
 universes u v
 variable {α : Type u}
@@ -224,6 +225,7 @@ attribute [to_additive gsmul_zero] one_gpow
 | (n+1:ℕ) := rfl
 | 0       := one_inv.symm
 | -[1+ n] := (inv_inv _).symm
+
 @[simp] theorem neg_gsmul : ∀ (a : β) (n : ℤ), -n • a = -(n • a) :=
 @gpow_neg (multiplicative β) _
 attribute [to_additive neg_gsmul] gpow_neg
@@ -297,6 +299,16 @@ theorem bit1_gsmul : ∀ (a : β) (n : ℤ), bit1 n • a = n • a + n • a +
 @gpow_bit1 (multiplicative β) _
 attribute [to_additive bit1_gsmul] gpow_bit1
 
+theorem gsmul_neg (a : β) (n : ℤ) : gsmul n (- a) = - gsmul n a :=
+begin
+  induction n using int.induction_on with z ih z ih,
+  { simp },
+  { rw [add_comm] {occs := occurrences.pos [1]}, simp [add_gsmul, ih, -add_comm] },
+  { rw [sub_eq_add_neg, add_comm] {occs := occurrences.pos [1]},
+    simp [ih, add_gsmul, neg_gsmul, -add_comm] }
+end
+attribute [to_additive gsmul_neg] gpow_neg
+
 end group
 
 namespace is_group_hom
@@ -308,10 +320,27 @@ by induction n with n ih; [exact is_group_hom.one f,
 
 theorem gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
 by cases n; [exact is_group_hom.pow f _ _,
-exact (is_group_hom.inv f _).trans (congr_arg _ $ is_group_hom.pow f _ _)]
+  exact (is_group_hom.inv f _).trans (congr_arg _ $ is_group_hom.pow f _ _)]
 
 end is_group_hom
 
+namespace is_add_group_hom
+variables {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f]
+
+theorem smul (a : α) (n : ℕ) : f (n • a) = n • f a :=
+by induction n with n ih; [exact is_add_group_hom.zero f,
+  rw [succ_smul, is_add_group_hom.add f, ih]]; refl
+
+theorem gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
+begin
+  induction n using int.induction_on with z ih z ih,
+  { simp [is_add_group_hom.zero f] },
+  { simp [is_add_group_hom.add f, add_gsmul, ih] },
+  { simp [is_add_group_hom.add f, is_add_group_hom.neg f, add_gsmul, ih] }
+end
+
+end is_add_group_hom
+
 local infix ` •ℤ `:70 := gsmul
 
 section comm_monoid
@@ -324,8 +353,21 @@ theorem gsmul_add : ∀ (a b : β) (n : ℤ), n •ℤ (a + b) = n •ℤ a + n
 @mul_gpow (multiplicative β) _
 attribute [to_additive gsmul_add] mul_gpow
 
+theorem gsmul_sub : ∀ (a b : β) (n : ℤ), gsmul n (a - b) = gsmul n a - gsmul n b :=
+by simp [gsmul_add, gsmul_neg]
+
 end comm_monoid
 
+section group
+
+@[instance]
+theorem is_add_group_hom_gsmul
+  {α β} [add_group α] [add_comm_group β] (f : α → β) [is_add_group_hom f] (z : ℤ) :
+  is_add_group_hom (λa, gsmul z (f a)) :=
+⟨assume a b, by rw [is_add_group_hom.add f, gsmul_add]⟩
+
+end group
+
 theorem add_monoid.smul_eq_mul' [semiring α] (a : α) (n : ℕ) : n • a = a * n :=
 by induction n with n ih; [rw [add_monoid.zero_smul, nat.cast_zero, mul_zero],
   rw [succ_smul', ih, nat.cast_succ, mul_add, mul_one]]
diff --git a/algebra/pi_instances.lean b/algebra/pi_instances.lean
index d98827d9e1ed2..6f774ad6e8fe3 100644
--- a/algebra/pi_instances.lean
+++ b/algebra/pi_instances.lean
@@ -5,8 +5,10 @@ Authors: Simon Hudon, Patrick Massot
 
 Pi instances for algebraic structures.
 -/
-
-import algebra.module order.basic tactic.pi_instances algebra.group
+import order.basic
+import algebra.module algebra.group
+import data.finset
+import tactic.pi_instances
 
 namespace pi
 universes u v
@@ -20,18 +22,27 @@ instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) := ⟨λ i,
 instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ i, 1⟩
 @[simp] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
 
+attribute [to_additive pi.has_zero] pi.has_one
+attribute [to_additive pi.zero_apply] pi.one_apply
+
 instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ x y, λ i, x i + y i⟩
 @[simp] lemma add_apply [∀ i, has_add $ f i] : (x + y) i = x i + y i := rfl
 
 instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ x y, λ i, x i * y i⟩
 @[simp] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
 
+attribute [to_additive pi.has_add] pi.has_mul
+attribute [to_additive pi.add_apply] pi.mul_apply
+
 instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ x, λ i, (x i)⁻¹⟩
 @[simp] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
 
 instance has_neg [∀ i, has_neg $ f i] : has_neg (Π i : I, f i) := ⟨λ x, λ i, -(x i)⟩
 @[simp] lemma neg_apply [∀ i, has_neg $ f i] : (-x) i = -x i := rfl
 
+attribute [to_additive pi.has_neg] pi.has_inv
+attribute [to_additive pi.neg_apply] pi.inv_apply
+
 instance has_scalar {α : Type*} [∀ i, has_scalar α $ f i] : has_scalar α (Π i : I, f i) := ⟨λ s x, λ i, s • (x i)⟩
 @[simp] lemma smul_apply {α : Type*} [∀ i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl
 
@@ -69,6 +80,32 @@ by pi_instance
 instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_comm_monoid $ f i] : ordered_cancel_comm_monoid (Π i : I, f i) :=
 by pi_instance
 
+attribute [to_additive pi.add_semigroup]              pi.semigroup
+attribute [to_additive pi.add_comm_semigroup]         pi.comm_semigroup
+attribute [to_additive pi.add_monoid]                 pi.monoid
+attribute [to_additive pi.add_comm_monoid]            pi.comm_monoid
+attribute [to_additive pi.add_group]                  pi.group
+attribute [to_additive pi.add_comm_group]             pi.comm_group
+attribute [to_additive pi.add_left_cancel_semigroup]  pi.left_cancel_semigroup
+attribute [to_additive pi.add_right_cancel_semigroup] pi.right_cancel_semigroup
+
+@[to_additive pi.list_sum_apply]
+lemma list_prod_apply {α : Type*} {β} [monoid β] (a : α) :
+  ∀ (l : list (α → β)), l.prod a = (l.map (λf:α → β, f a)).prod
+| []       := rfl
+| (f :: l) := by simp [mul_apply f l.prod a, list_prod_apply l]
+
+@[to_additive pi.multiset_sum_apply]
+lemma multiset_prod_apply {α : Type*} {β} [comm_monoid β] (a : α) (s : multiset (α → β)) :
+  s.prod a = (s.map (λf:α → β, f a)).prod :=
+quotient.induction_on s $ assume l, begin simp [list_prod_apply a l] end
+
+@[to_additive pi.finset_sum_apply]
+lemma finset_prod_apply {α : Type*} {β γ} [comm_monoid β] (a : α) (s : finset γ) (g : γ → α → β) :
+  s.prod g a = s.prod (λc, g c a) :=
+show (s.val.map g).prod a = (s.val.map (λc, g c a)).prod,
+  by rw [multiset_prod_apply, multiset.map_map]
+
 end pi
 
 namespace prod
diff --git a/group_theory/subgroup.lean b/group_theory/subgroup.lean
index cda9d7cd41c95..e31ed95b9d040 100644
--- a/group_theory/subgroup.lean
+++ b/group_theory/subgroup.lean
@@ -128,6 +128,10 @@ lemma mul_mem_cancel_right (h : a ∈ s) : a * b ∈ s ↔ b ∈ s :=
 
 end is_subgroup
 
+theorem is_add_subgroup.sub_mem {α} [add_group α] (s : set α) [is_add_subgroup s] (a b : α)
+  (ha : a ∈ s) (hb : b ∈ s) : a - b ∈ s :=
+is_add_submonoid.add_mem ha (is_add_subgroup.neg_mem hb)
+
 namespace group
 open is_submonoid is_subgroup
 
diff --git a/group_theory/submonoid.lean b/group_theory/submonoid.lean
index 9324bd6d3a5bc..0ef804657ea86 100644
--- a/group_theory/submonoid.lean
+++ b/group_theory/submonoid.lean
@@ -3,7 +3,8 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro
 -/
-import algebra.group_power
+import algebra.big_operators
+import data.finset
 import tactic.subtype_instance
 
 variables {α : Type*} [monoid α] {s : set α}
@@ -73,13 +74,37 @@ attribute [to_additive is_add_submonoid.multiple_subset] is_add_submonoid.multip
 
 end powers
 
+namespace is_submonoid
+
 @[to_additive is_add_submonoid.list_sum_mem]
-lemma is_submonoid.list_prod_mem [is_submonoid s] : ∀{l : list α}, (∀x∈l, x ∈ s) → l.prod ∈ s
-| []     h := is_submonoid.one_mem s
+lemma list_prod_mem [is_submonoid s] : ∀{l : list α}, (∀x∈l, x ∈ s) → l.prod ∈ s
+| []     h := one_mem s
 | (a::l) h :=
   suffices a * l.prod ∈ s, by simpa,
   have a ∈ s ∧ (∀x∈l, x ∈ s), by simpa using h,
-  is_submonoid.mul_mem this.1 (is_submonoid.list_prod_mem this.2)
+  is_submonoid.mul_mem this.1 (list_prod_mem this.2)
+
+@[to_additive is_add_submonoid.multiset_sum_mem]
+lemma multiset_prod_mem {α} [comm_monoid α] (s : set α) [is_submonoid s] (m : multiset α) :
+  (∀a∈m, a ∈ s) → m.prod ∈ s :=
+begin
+  refine quotient.induction_on m (assume l hl, _),
+  rw [multiset.quot_mk_to_coe, multiset.coe_prod],
+  exact list_prod_mem hl
+end
+
+@[to_additive is_add_submonoid.finset_sum_mem]
+lemma finset_prod_mem {α β} [comm_monoid α] (s : set α) [is_submonoid s] (f : β → α) :
+  ∀(t : finset β), (∀b∈t, f b ∈ s) → t.prod f ∈ s
+| ⟨m, hm⟩ hs :=
+  begin
+    refine multiset_prod_mem s _ _,
+    simp,
+    rintros a b hb rfl,
+    exact hs _ hb
+  end
+
+end is_submonoid
 
 instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
 by subtype_instance