log_eq_zero — Mathlib

English

The equation log x = 0 holds exactly when x ∈ {0, 1, -1}.

Русский

Уравнение log x = 0 выполняется ровно для x ∈ {0, 1, -1}.

LaTeX

$$$\\\\log x = 0 \\\\iff x = 0 \\\\lor x = 1 \\\\lor x = -1$$$

Lean4

@[simp]
theorem log_eq_zero {x : ℝ} : log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1 :=
  by
  constructor
  · intro h
    rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
    · refine Or.inr (Or.inr (neg_eq_iff_eq_neg.mp ?_))
      rw [← log_neg_eq_log x] at h
      exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h
    · exact Or.inl rfl
    · exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))
  · rintro (rfl | rfl | rfl) <;> simp only [log_one, log_zero, log_neg_eq_log]

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