logDeriv_eq_zero — Mathlib

English

The log derivative vanishes exactly when the underlying derivative vanishes.

Русский

Логарифмический дериватив равен нулю тогда и только тогда, когда производная элемента равна нулю.

LaTeX

$$$\\logDeriv a = 0 \\iff a' = 0$$$

Lean4

theorem logDeriv_eq_zero : logDeriv a = 0 ↔ a′ = 0 :=
  ⟨fun h ↦ by simp only [logDeriv, _root_.div_eq_zero_iff] at h; rcases h with h | h <;> simp [h], fun h ↦ by
    unfold logDeriv at *; simp [h]⟩

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