Theorem logDeriv_tprod_eq_tsum

Modification history

2026-02-05 18:04
Mathlib/Analysis/Calculus/LogDerivUniformlyOn.lean
feat(NumberTheory/ModularForms/DedekindEta): Show logDeriv eta is E2 (#34217) …
Modified logDeriv_tprod_eq_tsumView on Github →
2025-09-10 11:05
Mathlib/Analysis/Calculus/LogDerivUniformlyOn.lean
Log deriv lemmas (#28412)
Added logDeriv_tprod_eq_tsumView on Github →