Commit 2023-11-10 20:41 3901cb55

View on Github →

feat: characterize summability by vanishing of tsums (#8194)

Estimated changes

Modified Mathlib/Analysis/Calculus/Series.lean

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

modified theorem HasSum.unique

added theorem Summable.nat_tsum_vanishing

added theorem Summable.tsum_vanishing

added theorem cauchySeq_finset_iff_nat_tsum_vanishing

added theorem cauchySeq_finset_iff_tsum_vanishing

modified theorem cauchySeq_finset_iff_vanishing

modified theorem summable_iff_cauchySeq_finset

added theorem summable_iff_nat_tsum_vanishing

added theorem summable_iff_tsum_vanishing

modified theorem tendsto_tsum_compl_atTop_zero

modified theorem tsum_eq_add_tsum_ite'