---
tag: 0V948DE5KA
kind: statement
role: corollary
name: Logarithm of a power
msc: [33B10]
uses: [0K2FNY6DYV]
sources:
  - url: https://en.wikipedia.org/wiki/Natural_logarithm
    locator: Definition and properties
---

## Statement

For every real $x > 0$ and every natural number $n$,
$$\ln(x^n) = n \ln x.$$

## Remarks

Induction on $n$ with the [[product rule for logarithms|0K2FNY6DYV]] gives the claim.
For [[real exponents|0TV07AQT62]], $\ln(x^a) = a \ln x$ holds by the definition $x^a = e^{a \ln x}$.
Mathlib states it as `Real.log_pow`.

## Explanations

### L1 human

The logarithm brings an exponent down as a factor.
For example, $\ln(x^3) = 3 \ln x$.