feat(group_theory/submonoid/membership): upgrade definition of pow fr…

…om a set morphism to a monoid morphism (#10898)

This comes at no extra cost. All the prerequisite definitions and lemmas were already in mathlib.

src/group_theory/submonoid/membership.lean

@@ -220,7 +220,8 @@ lemma powers_subset {n : M} {P : submonoid M} (h : n ∈ P) : powers n ≤ P :=
 λ x hx, match x, hx with _, ⟨i, rfl⟩ := P.pow_mem h i end
 
 /-- Exponentiation map from natural numbers to powers. -/
-def pow (n : M) (m : ℕ) : powers n := ⟨n ^ m, m, rfl⟩
+@[simps] def pow (n : M) (m : ℕ) : powers n :=
+(powers_hom M n).mrange_restrict (multiplicative.of_add m)
 
 /-- Logarithms from powers to natural numbers. -/
 def log [decidable_eq M] {n : M} (p : powers n) : ℕ :=
@@ -237,8 +238,19 @@ theorem log_pow_eq_self [decidable_eq M] {n : M} (h : function.injective (λ m :
   log (pow n m) = m :=
 pow_right_injective_iff_pow_injective.mp h $ pow_log_eq_self _
 
+/-- The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers
+when it is injective. The inverse is given by the logarithms. -/
+@[simps]
+def pow_log_equiv [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m)) :
+  multiplicative ℕ ≃* powers n :=
+{ to_fun := λ m, pow n m.to_add,
+  inv_fun := λ m, multiplicative.of_add (log m),
+  left_inv := log_pow_eq_self h,
+  right_inv := pow_log_eq_self,
+  map_mul' := λ _ _, by { simp only [pow, map_mul, of_add_add, to_add_mul] } }
+
 theorem log_pow_int_eq_self {x : ℤ} (h : 1 < x.nat_abs) (m : ℕ) : log (pow x m) = m :=
-log_pow_eq_self (int.pow_right_injective h) _
+(pow_log_equiv (int.pow_right_injective h)).symm_apply_apply _
 
 @[simp] lemma map_powers {N : Type*} [monoid N] (f : M →* N) (m : M) :
   (powers m).map f = powers (f m) :=