Commit 2023-10-25 01:20 6c712437

View on Github →

chore: move tendsto_zpow_atTop_atTop (#7887) Also move it to the Filter namespace and drop Strict from some TC assumptions.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

deleted theorem tendsto_zpow_atTop_atTop

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.tendsto_zpow_atTop_atTop