Theorem tendsto_rpow_atTop_of_base_gt_one

Modification history

2026-07-05 18:40
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
feat(Analysis/SpecialFunctions/Pow/Asymptotics): add Real.tendsto_rpow_atTop_of_base_gt_one (#41375) …
Added tendsto_rpow_atTop_of_base_gt_oneView on Github →
2025-08-25 02:15
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
chore(Analysis/SpecialFunctions/Pow) deprecate misnamed duplicate tendsto_rpow_atTop_of_base_gt_one (#28870) …
Deleted tendsto_rpow_atTop_of_base_gt_oneView on Github →
2023-08-13 08:12
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
feat: lemmas about monotonicity and asymptotics of `rpow` (#6140)
Added tendsto_rpow_atTop_of_base_gt_oneView on Github →