Theorem Real.not_differentiableAt_inv_log_zero

Modification history

2025-12-27 08:07
Mathlib/Analysis/SpecialFunctions/Log/InvLog.lean
feat(NumberTheory.Chebyshev): prove connection between prime counting and theta (#32281) …
Added Real.not_differentiableAt_inv_log_zeroView on Github →