log_eq_zero_iff

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

For any base b and n, log(b, n) = 0 if and only if n < b or b ≤ 1.

Русский

Для любых b, n: log_b(n) = 0 тогда и только если n < b или b ≤ 1.

LaTeX

$$$\\log_b(n) = 0 \\iff n < b \\ \\lor\\ b \\le 1.$$$

Lean4

@[simp]
theorem log_eq_zero_iff {b n : ℕ} : log b n = 0 ↔ n < b ∨ b ≤ 1 :=
  by
  rw [log, dite_eq_right_iff]
  simp only [Nat.add_eq_zero_iff, Nat.one_ne_zero, and_false, imp_false, not_and_or, not_le, not_lt]

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

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

Разделы

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

Аффилиация

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