Commit 2025-09-10 11:05 76dc62ec

View on Github →

Log deriv lemmas (#28412)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

added theorem Set.EqOn.deriv

Modified Mathlib/Analysis/Calculus/LogDeriv.lean

added theorem logDeriv_eqOn_iff

Created Mathlib/Analysis/Calculus/LogDerivUniformlyOn.lean

added theorem logDeriv_tprod_eq_tsum