log_of_left_le_one — Mathlib

English

If the base b is at most 1, then the logarithm of any element r is 0. In other words, log_b r = 0 whenever b ≤ 1.

Русский

Если основание b не больше 1, то логарифм любого элемента r равен нулю: log_b r = 0 при b ≤ 1.

LaTeX

$$$\log_b r = 0 \quad\text{если } b \le 1$$$

Lean4

theorem log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (r : R) : log b r = 0 :=
  by
  rcases le_total 1 r with h | h
  · rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, Int.ofNat_zero]
  · rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]

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