Theorem AbsoluteValue.tendsto_div_one_add_pow_nhds_one

Modification history

2025-10-01 10:39
Mathlib/Analysis/SpecificLimits/Normed.lean
feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 (#27969) …
Added AbsoluteValue.tendsto_div_one_add_pow_nhds_oneView on Github →