Theorem Real.isBigO_log_const_mul_log_atTop

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