clog_zero_right

Mathlib.Data.Int.Log

URI: https://scilib.ai/kg/mathlib#Int.clog_zero_right

English

For any base b, clog_b(0) = 0.

Русский

Для любого основания clog_b(0) = 0.

LaTeX

$$$\operatorname{clog}_b(0)=0$$$

Lean4

@[simp]
theorem clog_zero_right (b : ℕ) : clog b (0 : R) = 0 :=
  clog_of_right_le_zero _ le_rfl

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

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

Разделы

Аффилиация

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