clog_zero_left

Mathlib.Data.Int.Log

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

← MathLib Explorer

English

For any r, clog_0(r) = 0.

Русский

Для основания 0 выполняется clog_0(r) = 0.

LaTeX

$$$\operatorname{clog}_0(r)=0$$$

Lean4

@[simp]
theorem clog_zero_left (r : R) : clog 0 r = 0 := by
  by_cases hr : 1 ≤ r
  · simp only [clog, Nat.clog_zero_left, Nat.cast_zero, Nat.log_zero_left, neg_zero, ite_self]
  · simp only [clog, hr, ite_cond_eq_false, Nat.log_zero_left, Nat.cast_zero, neg_zero]

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

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

Разделы

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

Аффилиация

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