log_of_nat_eq_posLog

Mathlib.Analysis.SpecialFunctions.Log.PosLog

URI: https://scilib.ai/kg/mathlib#Real.log_of_nat_eq_posLog

← MathLib Explorer

English

log⁺ n = log n for natural numbers n.

Русский

log⁺ n = log n для натуральных чисел n.

LaTeX

$$log^{+} n = \log n$$

Lean4

/-- The function `log⁺` equals `log` for all natural numbers. -/
theorem log_of_nat_eq_posLog {n : ℕ} : log⁺ n = log n :=
  by
  by_cases hn : n = 0
  · simp [hn, posLog]
  · simp [posLog_eq_log, Nat.one_le_iff_ne_zero.2 hn]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru