logb_self_eq_one

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

If the base b is greater than 1, then the logarithm of the base taken at the base itself is 1.

Русский

Если основание b больше 1, то log_b(b) = 1.

LaTeX

$$$\log_b b = 1 \quad (1 < b)$$$

Lean4

@[simp]
theorem logb_self_eq_one (hb : 1 < b) : logb b b = 1 :=
  div_self (log_pos hb).ne'

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

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

Разделы

Аффилиация

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