log_two_bit

Mathlib.Data.Nat.Log

URI: https://scilib.ai/kg/mathlib#Nat.log_two_bit

← MathLib Explorer

English

For any base-2 logarithm, log_2(n.bit b) = log_2(n) + 1 when n ≠ 0.

Русский

Для логарифма по основанию 2 выполняется log_2(n.bit b) = log_2(n) + 1 при n ≠ 0.

LaTeX

$$$ (n \neq 0) \Rightarrow \log_2(n\text{.bit } b) = \log_2 n + 1 $$$

Lean4

theorem log_two_bit {b n} (hn : n ≠ 0) : Nat.log 2 (n.bit b) = Nat.log 2 n + 1 := by
  rw [← log_div_mul_self, bit_div_two, log_mul_base Nat.one_lt_two hn]

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

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

Разделы

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

Аффилиация

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