Theorem Real.differentiableOn_log_log'

Modification history

2026-07-08 03:27
Mathlib/Analysis/SpecialFunctions/Log/InvLog.lean
feat(Analysis/SpecialFunctions/Log/InvLog): add more API for inv_log and log_log (#40847) …
Added Real.differentiableOn_log_log'View on Github →