Theorem tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded

Modification history

2026-01-20 08:34

Mathlib/Analysis/SpecificLimits/Normed.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …

Modified tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded View on Github →

2025-05-22 00:24

Mathlib/Analysis/SpecificLimits/Normed.lean

feat(Analysis/SpecialFunctions): extend `tendsto_one_plus_div_rpow_exp` (#23804) …

Added tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded View on Github →