Theorem Real.isBigO_logb_log

Modification history

2026-02-10 18:25

Mathlib/Analysis/SpecialFunctions/Log/Base.lean

feat(Mathlib/Analysis/SpecialFunctions/Log/Base): More log asymptotics (#33389) …

Added Real.isBigO_logb_log View on Github →