log_div_base — Mathlib

English

For all b,n ≥ 1, log_b(n) and log_b(n/b) satisfy log_b(n/b) = log_b(n) − 1.

Русский

Для любого b>1 и любого n верно log_b(n/b) = log_b(n) − 1.

LaTeX

$$$\log_b(n/b) = \log_b n - 1$$$

Lean4

@[simp]
theorem log_div_base (b n : ℕ) : log b (n / b) = log b n - 1 :=
  by
  rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
  rcases lt_or_ge n b with h | h
  · rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
  rw [log_of_one_lt_of_le hb h, Nat.add_sub_cancel_right]

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