feat(algebra/group_power): Add mul/add variants of powers_hom and fri…

…ends (#4636)

src/algebra/group_power/lemmas.lean

@@ -8,6 +8,7 @@ import algebra.opposites
 import data.list.basic
 import data.int.cast
 import data.equiv.basic
+import data.equiv.mul_add
 import deprecated.group
 
 /-!
@@ -459,6 +460,54 @@ by rw [← gmultiples_hom_symm_apply, ← gmultiples_hom_apply, equiv.apply_symm
 
 /-! `add_monoid_hom.ext_int` is defined in `data.int.cast` -/
 
+variables (M G A)
+
+/-- If `M` is commutative, `powers_hom` is a multiplicative equivalence. -/
+def powers_mul_hom [comm_monoid M] : M ≃* (multiplicative ℕ →* M) :=
+{ map_mul' := λ a b, monoid_hom.ext $ by simp [mul_pow],
+  ..powers_hom M}
+
+/-- If `M` is commutative, `gpowers_hom` is a multiplicative equivalence. -/
+def gpowers_mul_hom [comm_group G] : G ≃* (multiplicative ℤ →* G) :=
+{ map_mul' := λ a b, monoid_hom.ext $ by simp [mul_gpow],
+  ..gpowers_hom G}
+
+/-- If `M` is commutative, `multiples_hom` is an additive equivalence. -/
+def multiples_add_hom [add_comm_monoid A] : A ≃+ (ℕ →+ A) :=
+{ map_add' := λ a b, add_monoid_hom.ext $ by simp [nsmul_add],
+  ..multiples_hom A}
+
+/-- If `M` is commutative, `gmultiples_hom` is an additive equivalence. -/
+def gmultiples_add_hom [add_comm_group A] : A ≃+ (ℤ →+ A) :=
+{ map_add' := λ a b, add_monoid_hom.ext $ by simp [gsmul_add],
+  ..gmultiples_hom A}
+
+variables {M G A}
+
+@[simp] lemma powers_mul_hom_apply [comm_monoid M] (x : M) (n : multiplicative ℕ) :
+  powers_mul_hom M x n = x ^ n.to_add := rfl
+
+@[simp] lemma powers_mul_hom_symm_apply [comm_monoid M] (f : multiplicative ℕ →* M) :
+  (powers_mul_hom M).symm f = f (multiplicative.of_add 1) := rfl
+
+@[simp] lemma gpowers_mul_hom_apply [comm_group G] (x : G) (n : multiplicative ℤ) :
+  gpowers_mul_hom G x n = x ^ n.to_add := rfl
+
+@[simp] lemma gpowers_mul_hom_symm_apply [comm_group G] (f : multiplicative ℤ →* G) :
+  (gpowers_mul_hom G).symm f = f (multiplicative.of_add 1) := rfl
+
+@[simp] lemma multiples_add_hom_apply [add_comm_monoid A] (x : A) (n : ℕ) :
+  multiples_add_hom A x n = n •ℕ x := rfl
+
+@[simp] lemma multiples_add_hom_symm_apply [add_comm_monoid A] (f : ℕ →+ A) :
+  (multiples_add_hom A).symm f = f 1 := rfl
+
+@[simp] lemma gmultiples_add_hom_apply [add_comm_group A] (x : A) (n : ℤ) :
+  gmultiples_add_hom A x n = n •ℤ x := rfl
+
+@[simp] lemma gmultiples_add_hom_symm_apply [add_comm_group A] (f : ℤ →+ A) :
+  (gmultiples_add_hom A).symm f = f 1 := rfl
+
 /-!
 ### Commutativity (again)