log_pow — Mathlib

English

For x > 0 and n ∈ ℕ, log(x^n) = n log x.

Русский

Для x > 0 и n ∈ ℕ верно log(x^n) = n log x.

LaTeX

$$$x > 0 \\\\land n \\in \\\\mathbb{N} \\\\Rightarrow \\\\log(x^n) = n \\\\log x$$$

Lean4

@[simp]
theorem log_pow (x : ℝ) (n : ℕ) : log (x ^ n) = n * log x := by
  induction n with
  | zero => simp
  | succ n ih =>
    rcases eq_or_ne x 0 with (rfl | hx)
    · simp
    · rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]

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