Theorems · Definition · group theory

Submonoid.powLogEquiv

{M : Type u_1} →
  [inst : Monoid M] →
    [DecidableEq M] → {n : M} → (Function.Injective fun m => n ^ m) → Multiplicative ℕ ≃* ↥(Submonoid.powers n)

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.

Defined in

Mathlib.Algebra.Group.Submonoid.Membership

Cited by

4 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidDecidableEq