log — Mathlib

English

Define log as an arithmetic function log: ℕ → ℝ by log(n) = ln(n).

Русский

Определим логарифм как арифметическую функцию log: ℕ → ℝ по формуле log(n) = ln(n).

LaTeX

$$$$\log(n) = \ln n, \quad n \in \mathbb{N}.$$$$

Lean4

/-- `log` as an arithmetic function `ℕ → ℝ`. Note this is in the `ArithmeticFunction`
namespace to indicate that it is bundled as an `ArithmeticFunction` rather than being the usual
real logarithm. -/
noncomputable def log : ArithmeticFunction ℝ :=
  ⟨fun n => Real.log n, by simp⟩

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