clog_one_left

Mathlib.Data.Int.Log

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

English

For any r, clog_1(r) = 0.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem clog_one_left (r : R) : clog 1 r = 0 := by
  simp only [clog, Nat.log_one_left, Nat.cast_zero, Nat.clog_one_left, neg_zero, ite_self]

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

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

Разделы

Аффилиация

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