logb_self_eq_one_iff

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

The equation log_b(b) = 1 holds precisely when b ≠ 0, b ≠ 1, and b ≠ -1.

Русский

Уравнение log_b(b) = 1 выполняется тогда и только тогда, когда b ≠ 0, b ≠ 1 и b ≠ −1.

LaTeX

$$$\log_b b = 1 \iff b \neq 0 \land b \neq 1 \land b \neq -1$$$

Lean4

theorem logb_self_eq_one_iff : logb b b = 1 ↔ b ≠ 0 ∧ b ≠ 1 ∧ b ≠ -1 :=
  Iff.trans ⟨fun h h' => by simp [logb, h'] at h, div_self⟩ log_ne_zero

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

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

Разделы

Аффилиация

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