Commit 2025-11-26 12:23 01940078

View on Github →

feat(Analysis): tendsto_zpow_nhdsNE_zero_cobounded (#32120)

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Order.lean

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

added theorem Filter.inv_nhdsNE_zero

deleted theorem Filter.inv_nhdsWithin_ne_zero

added theorem Filter.tendsto_inv₀_nhdsNE_zero

deleted theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero

deleted theorem NormedField.tendsto_norm_inv_nhdsNE_zero_atTop

added theorem tendsto_norm_inv_nhdsNE_zero_atTop

added theorem tendsto_zpow_nhdsNE_zero_cobounded

Modified Mathlib/Analysis/Normed/Ring/Lemmas.lean

added theorem tendsto_pow_cobounded_cobounded