log_nz_of_isRat_neg — Mathlib

English

If e is a rat representation with negative ratio, then log e ≠ 0.

Русский

Если e представлено как рациональное число с отрицательным отношением, то log e ≠ 0.

LaTeX

$$$$ \\log e \\neq 0. $$$$

Lean4

theorem log_nz_of_isRat_neg {n : ℤ} :
    (NormNum.IsRat e n d) → (decide (n / d < (0 : ℚ))) → (decide ((-1 : ℚ) < n / d)) → (Real.log (e : ℝ) ≠ 0)
  | ⟨inv, eq⟩, h₁, h₂ => by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have h₁' : (n : ℝ) / d < 0 := by exact_mod_cast of_decide_eq_true h₁
    have h₂' : -1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₂
    exact ne_of_lt <| Real.log_neg_of_lt_zero h₁' h₂'

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