Commit 2024-11-12 17:08 15ae5b0c

View on Github →

feat: add two limit results (#16545)

Estimated changes

Modified Mathlib/Analysis/PSeries.lean

added theorem summable_pow_div_add

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

added theorem tendsto_const_div_pow

Modified Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

added theorem HasSum.const_div

added theorem Summable.const_div

added theorem hasSum_const_div_iff

added theorem summable_const_div_iff

Modified Mathlib/Topology/Algebra/Order/Field.lean

added theorem Filter.Tendsto.const_div_atTop