log_div_mul_self — Mathlib

English

For all b,n, log_b(n / b * b) = log_b(n).

Русский

Для всех b,n верно log_b(n / b • b) = log_b(n).

LaTeX

$$$\log_b(n / b \cdot b) = \log_b n$$$

Lean4

@[simp]
theorem log_div_mul_self (b n : ℕ) : log b (n / b * b) = log b n :=
  by
  rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb, log_of_left_le_one hb]
  rcases lt_or_ge n b with h | h
  · rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
  rw [log_mul_base hb (Nat.div_pos h (by cutsat)).ne', log_div_base, Nat.sub_add_cancel (succ_le_iff.2 <| log_pos hb h)]

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