Theorem Real.inv_log_isLittleO_one

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.inv_log_isLittleO_one View on Github →