log_pow_int_eq_self — Mathlib

English

For integer bases x with |x|>1, log of n-th power equals n for appropriate n in natural numbers (specialized to integers).

Русский

Для целочисленной основы x со свойством |x|>1 логарифм степени равен соответствующему числу n над naturals.

LaTeX

$$$ \\log(\\text{pow}_{\\mathbb{Z}}(x,m)) = m \\quad (1 < |x|) $$$

Lean4

theorem log_pow_int_eq_self {x : ℤ} (h : 1 < x.natAbs) (m : ℕ) : log (pow x m) = m :=
  (powLogEquiv (Int.pow_right_injective h)).symm_apply_apply _

Похожие утверждения