Commit 2024-08-22 08:20 87e5ef38

View on Github →

chore: tag more differentiability lemmas about log with fun_prop (#16027) From LeanAPAP

Estimated changes

modified theorem Real.differentiableAt_log