Theorem Asymptotics.IsBigO.pow_of_le_right

Modification history

2025-11-05 05:40
Mathlib/Analysis/Asymptotics/Lemmas.lean
feat(Analysis/Distribution): basic algebraic properties of functions of temperate growth (#31112)
Added Asymptotics.IsBigO.pow_of_le_rightView on Github →