Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-11 23:46 f0ae67d0

View on Github →

feat(analysis/normed_space/finite_dimension): asymptotic equivalence preserves summability (#8596)

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

modified theorem summable_of_is_O

modified theorem summable_of_is_O_nat

Modified src/analysis/normed_space/finite_dimension.lean

added theorem is_equivalent.summable_iff

added theorem is_equivalent.summable_iff_nat

added theorem summable_of_is_O'

added theorem summable_of_is_O_nat'

added theorem summable_of_is_equivalent

added theorem summable_of_is_equivalent_nat

Modified src/analysis/specific_limits.lean

Modified src/topology/algebra/infinite_sum.lean

added theorem summable.trans_sub

added theorem summable_iff_of_summable_sub