Commit 2025-08-25 02:15 374af904

chore(Analysis/SpecialFunctions/Pow) deprecate misnamed duplicate tendsto_rpow_atTop_of_base_gt_one (#28870) #6140 added both tendsto_rpow_atTop_of_base_gt_one and tendsto_rpow_atBot_of_base_gt_one. These two theorems have the same type and had (until #28371) nearly identical proofs. It seems clear that the atTop part of the former's name is an error, and that these were not intended to be separate theorems.