log_eq_zero — Mathlib

English

If o < b, then log b o = 0.

Русский

Если o < b, то log_b o = 0.

LaTeX

$$$ o < b \Rightarrow \log_b o = 0 $$$

Lean4

theorem log_eq_zero {b o : Ordinal} (hbo : o < b) : log b o = 0 :=
  by
  rcases eq_or_ne o 0 with (rfl | ho)
  · exact log_zero_right b
  rcases le_or_gt b 1 with hb | hb
  · rcases le_one_iff.1 hb with (rfl | rfl)
    · exact log_zero_left o
    · exact log_one_left o
  · rwa [← Ordinal.le_zero, ← lt_succ_iff, succ_zero, ← lt_opow_iff_log_lt hb ho, opow_one]

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