∀ {M : Type u_1} [inst : Monoid M] [inst_1 : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m)
  (m : ↥(Submonoid.powers n)), (Submonoid.powLogEquiv h).symm m = Multiplicative.ofAdd (Submonoid.log m)