feat(algebra/group_power): smul and pow are monoid homs

src/algebra/group_power.lean

@@ -124,6 +124,26 @@ by induction n; simp [*, pow_succ]
 
 end monoid
 
+namespace is_monoid_hom
+variables {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
+
+theorem map_pow (a : α) : ∀(n : ℕ), f (a ^ n) = (f a) ^ n
+| 0            := is_monoid_hom.map_one f
+| (nat.succ n) := by rw [pow_succ, is_monoid_hom.map_mul f, map_pow n]; refl
+
+end is_monoid_hom
+
+namespace is_add_monoid_hom
+variables {β : Type*} [add_monoid α] [add_monoid β] (f : α → β) [is_add_monoid_hom f]
+
+theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a)
+| 0            := is_add_monoid_hom.map_zero f
+| (nat.succ n) := by rw [succ_smul, is_add_monoid_hom.map_add f, map_smul n]; refl
+
+end is_add_monoid_hom
+
+attribute [to_additive is_add_monoid_hom.map_smul] is_monoid_hom.map_pow
+
 @[simp] theorem nat.pow_eq_pow (p q : ℕ) :
   @has_pow.pow _ _ monoid.has_pow p q = p ^ q :=
 by induction q with q ih; [refl, rw [nat.pow_succ, pow_succ, mul_comm, ih]]
@@ -335,8 +355,7 @@ namespace is_group_hom
 variables {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f]
 
 theorem pow (a : α) (n : ℕ) : f (a ^ n) = f a ^ n :=
-by induction n with n ih; [exact is_group_hom.one f,
-  rw [pow_succ, is_group_hom.mul f, ih]]; refl
+is_monoid_hom.map_pow f a n
 
 theorem gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
 by cases n; [exact is_group_hom.pow f _ _,
@@ -348,8 +367,7 @@ 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
+is_add_monoid_hom.map_smul f a n
 
 theorem gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
 begin