English
The exponentiation map is an isomorphism from the additive monoid of natural numbers to the submonoid of powers when injective; its inverse is given by log.
Русский
Карта возведения в степень является изоморфизмом между аддитивным моноидом натуральных чисел и подмоноидом степеней при инъективности; обратная карта задаётся логарифмом.
LaTeX
$$$ \\text{PowLogEquiv} : \\mathbb{N} \\cong* \\operatorname{powers}(n) $$$
Lean4
/-- 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 powLogEquiv [DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m) : Multiplicative ℕ ≃* powers n
where
toFun m := pow n m.toAdd
invFun m := Multiplicative.ofAdd (log m)
left_inv := log_pow_eq_self h
right_inv := pow_log_eq_self
map_mul' _ _ := by simp only [pow, map_mul, ofAdd_add, toAdd_mul]
