log_of_right_le_zero — Mathlib

English

If r ≤ 0, then log_b r = 0 for any base b. The logarithm vanishes on nonpositive arguments.

Русский

Если r ≤ 0, тогда log_b r = 0 для любого основания b. Логарифм равен нулю на неположительных аргументах.

LaTeX

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

Lean4

theorem log_of_right_le_zero (b : ℕ) {r : R} (hr : r ≤ 0) : log b r = 0 := by
  rw [log_of_right_le_one _ (hr.trans zero_le_one),
    Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one), Int.ofNat_zero, neg_zero]

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