feat(group_theory/submonoid/membership): add log, exp lemmas (#8870)

Breaking up a previous PR (#7843) into smaller ones.

This PR adds lemmas about injectivity of `pow` and `log` functions under appropriate conditions.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238870)

src/group_theory/submonoid/membership.lean

@@ -214,6 +214,27 @@ by { ext, exact mem_closure_singleton.symm }
 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⟩
+
+/-- Logarithms from powers to natural numbers. -/
+def log [decidable_eq M] {n : M} (p : powers n) : ℕ :=
+nat.find $ (mem_powers_iff p.val n).mp p.prop
+
+@[simp] theorem pow_log_eq_self [decidable_eq M] {n : M} (p : powers n) : pow n (log p) = p :=
+subtype.ext $ nat.find_spec p.prop
+
+lemma pow_right_injective_iff_pow_injective {n : M} :
+  function.injective (λ m : ℕ, n ^ m) ↔ function.injective (pow n) :=
+subtype.coe_injective.of_comp_iff (pow n)
+
+theorem log_pow_eq_self [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m)) (m : ℕ) :
+  log (pow n m) = m := 
+pow_right_injective_iff_pow_injective.mp h $ pow_log_eq_self _
+
+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) _
+
 end submonoid
 
 namespace submonoid