natCast_log — Mathlib

English

For natural numbers n, the real logarithm of n equals the complex logarithm of its complex representation.

Русский

Для натурального числа n выполняется равенство Real.log(n) = log(n) в связанных отображениях через комплексное число.

LaTeX

$$$$\\operatorname{Real.log}(\\operatorname{ofNat}(n)) = \\log(\\operatorname{OfNat.ofNat}(n)).$$$$

Lean4

@[simp, norm_cast]
theorem natCast_log {n : ℕ} : Real.log n = log n :=
  ofReal_natCast n ▸ ofReal_log n.cast_nonneg

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