Commit 2023-03-02 07:55 eab55756

View on Github →

feat: port Topology.Algebra.InfiniteSum.Basic (#2500)

Estimated changes

Modified Mathlib.lean

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

added theorem Equiv.hasSum_iff

added theorem Equiv.hasSum_iff_of_support

added theorem Equiv.summable_iff

added theorem Equiv.summable_iff_of_support

added theorem Equiv.tsum_eq

added theorem Equiv.tsum_eq_tsum_of_support

added theorem Finset.tsum_subtype'

added theorem Finset.tsum_subtype

added theorem Function.Injective.hasSum_iff

added theorem Function.Injective.hasSum_range_iff

added theorem Function.Injective.summable_iff

added theorem Function.Surjective.summable_iff_of_hasSum_iff

added theorem Function.Surjective.tsum_eq_tsum_of_hasSum_iff_hasSum

added theorem HasSum.add

added theorem HasSum.add_compl

added theorem HasSum.add_disjoint

added theorem HasSum.add_isCompl

added theorem HasSum.compl_add

added theorem HasSum.const_smul

added theorem HasSum.even_add_odd

added theorem HasSum.hasSum_compl_iff

added theorem HasSum.hasSum_iff_compl

added theorem HasSum.hasSum_of_sum_eq

added theorem HasSum.int_rec

added theorem HasSum.neg

added theorem HasSum.nonneg_add_neg

added theorem HasSum.op

added theorem HasSum.pos_add_zero_add_neg

added theorem HasSum.prod_fiberwise

added theorem HasSum.prod_mk

added theorem HasSum.sigma

added theorem HasSum.sigma_of_hasSum

added theorem HasSum.star

added theorem HasSum.sub

added theorem HasSum.sum_nat_of_sum_int

added theorem HasSum.summable

added theorem HasSum.tendsto_sum_nat

added theorem HasSum.tsum_eq

added theorem HasSum.unique

added theorem HasSum.unop

added theorem HasSum.update'

added theorem HasSum.update

added def HasSum

added theorem Pi.hasSum

added theorem Pi.summable

added theorem Set.Finite.summable_compl_iff

added theorem Summable.add

added theorem Summable.add_compl

added theorem Summable.comp_injective

added theorem Summable.compl_add

added theorem Summable.congr

added theorem Summable.const_smul

added theorem Summable.even_add_odd

added theorem Summable.hasSum

added theorem Summable.hasSum_iff

added theorem Summable.hasSum_iff_tendsto_nat

added theorem Summable.neg

added theorem Summable.ofStar

added theorem Summable.of_neg

added theorem Summable.op

added theorem Summable.prod_factor

added theorem Summable.prod_symm

added theorem Summable.sigma'

added theorem Summable.sigma

added theorem Summable.sigma_factor

added theorem Summable.star

added theorem Summable.sub

added theorem Summable.subtype

added theorem Summable.summable_compl_iff

added theorem Summable.summable_of_eq_zero_or_self

added theorem Summable.tendsto_atTop_zero

added theorem Summable.tendsto_cofinite_zero

added theorem Summable.trans_sub

added theorem Summable.unop

added theorem Summable.update

added theorem Summable.vanishing

added def Summable

added theorem cauchySeq_finset_iff_vanishing

added theorem eq_add_of_hasSum_ite

added theorem hasSum_empty

added theorem hasSum_fintype

added theorem hasSum_iff_hasSum

added theorem hasSum_iff_hasSum_of_ne_zero_bij

added theorem hasSum_ite_eq

added theorem hasSum_ite_sub_hasSum

added theorem hasSum_nat_add_iff'

added theorem hasSum_nat_add_iff

added theorem hasSum_op

added theorem hasSum_pi_single

added theorem hasSum_single

added theorem hasSum_subtype_iff_indicator

added theorem hasSum_subtype_iff_of_support_subset

added theorem hasSum_subtype_support

added theorem hasSum_sum

added theorem hasSum_sum_disjoint

added theorem hasSum_sum_of_ne_finset_zero

added theorem hasSum_unop

added theorem hasSum_zero

added theorem rel_sup_add

added theorem rel_supᵢ_sum

added theorem rel_supᵢ_tsum

added theorem sum_add_tsum_compl

added theorem sum_add_tsum_nat_add

added theorem sum_add_tsum_subtype_compl

added theorem sum_eq_tsum_indicator

added theorem summable_congr

added theorem summable_empty

added theorem summable_iff_cauchySeq_finset

added theorem summable_iff_of_summable_sub

added theorem summable_iff_vanishing

added theorem summable_int_of_summable_nat

added theorem summable_nat_add_iff

added theorem summable_neg_iff

added theorem summable_of_ne_finset_zero

added theorem summable_op

added theorem summable_star_iff'

added theorem summable_star_iff

added theorem summable_subtype_and_compl

added theorem summable_subtype_iff_indicator

added theorem summable_sum

added theorem summable_unop

added theorem summable_zero

added theorem tendsto_sum_nat_add

added theorem tendsto_tsum_compl_atTop_zero

added theorem tsum_add

added theorem tsum_add_tsum_compl

added theorem tsum_apply

added theorem tsum_bool

added theorem tsum_comm'

added theorem tsum_comm

added theorem tsum_congr

added theorem tsum_congr_subtype

added theorem tsum_const_smul

added theorem tsum_dite_left

added theorem tsum_dite_right

added theorem tsum_empty

added theorem tsum_eq_add_tsum_ite'

added theorem tsum_eq_add_tsum_ite

added theorem tsum_eq_single

added theorem tsum_eq_sum

added theorem tsum_eq_tsum_of_hasSum_iff_hasSum

added theorem tsum_eq_tsum_of_ne_zero_bij

added theorem tsum_eq_zero_add

added theorem tsum_eq_zero_of_not_summable

added theorem tsum_even_add_odd

added theorem tsum_finset_bUnion_disjoint

added theorem tsum_fintype

added theorem tsum_image

added theorem tsum_ite_eq

added theorem tsum_neg

added theorem tsum_op

added theorem tsum_pi_single

added theorem tsum_prod'

added theorem tsum_prod

added theorem tsum_range

added theorem tsum_sigma'

added theorem tsum_sigma

added theorem tsum_singleton

added theorem tsum_star

added theorem tsum_sub

added theorem tsum_subtype

added theorem tsum_subtype_add_tsum_subtype_compl

added theorem tsum_subtype_eq_of_support_subset

added theorem tsum_sum

added theorem tsum_supᵢ_decode₂

added theorem tsum_tsum_eq_single

added theorem tsum_union_disjoint

added theorem tsum_unionᵢ_decode₂

added theorem tsum_univ

added theorem tsum_unop

added theorem tsum_zero'

added theorem tsum_zero