clog_of_left_le_one

Mathlib.Data.Nat.Log

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

English

If b ≤ 1, then clog_b(n) = 0 for all n.

Русский

Если b ≤ 1, то clog_b(n) = 0 для любого n.

LaTeX

$$$ b \le 1 \Rightarrow \operatorname{clog}(b,n) = 0 $$$

Lean4

theorem clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n : ℕ) : clog b n = 0 := by
  rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.1.not_ge hb]

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

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

Разделы

Аффилиация

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