log_of_left_le_one

Mathlib.Data.Nat.Log

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

English

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

Русский

Если b ≤ 1, то log_b(n) = 0 для всех n.

LaTeX

$$$b \\le 1 \\Rightarrow \\log_b(n) = 0.$$$

Lean4

theorem log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n) : log b n = 0 :=
  log_eq_zero_iff.2 (Or.inr hb)

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

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

Разделы

Аффилиация

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