Commit 2024-02-29 08:53 10672055

View on Github →

chore(Topology/Algebra/InfiniteSum): split up large file (#11050) Split up Mathlib.Topology.Algebra.InfiniteSum.Basic (1600 lines) into smaller files.

Estimated changes

modified theorem HasSum.add
deleted theorem HasSum.const_smul
deleted theorem HasSum.even_add_odd
deleted theorem HasSum.hasSum_compl_iff
deleted theorem HasSum.hasSum_iff_compl
deleted theorem HasSum.int_rec
deleted theorem HasSum.neg
deleted theorem HasSum.nonneg_add_neg
deleted theorem HasSum.op
deleted theorem HasSum.prod_fiberwise
deleted theorem HasSum.prod_mk
deleted theorem HasSum.sigma
deleted theorem HasSum.sigma_of_hasSum
deleted theorem HasSum.star
deleted theorem HasSum.sub
deleted theorem HasSum.sum_nat_of_sum_int
deleted theorem HasSum.sum_range_add
deleted theorem HasSum.summable
deleted theorem HasSum.tendsto_sum_nat
deleted theorem HasSum.tsum_eq
deleted theorem HasSum.tsum_fiberwise
deleted theorem HasSum.unique
deleted theorem HasSum.unop
deleted theorem HasSum.update
deleted def HasSum
deleted theorem Pi.hasSum
deleted theorem Pi.summable
modified theorem Summable.add
deleted theorem Summable.comp_injective
deleted theorem Summable.const_smul
deleted theorem Summable.even_add_odd
deleted theorem Summable.hasSum
deleted theorem Summable.hasSum_iff
deleted theorem Summable.neg
deleted theorem Summable.ofStar
deleted theorem Summable.of_neg
deleted theorem Summable.op
deleted theorem Summable.prod_factor
deleted theorem Summable.prod_symm
deleted theorem Summable.sigma'
deleted theorem Summable.sigma
deleted theorem Summable.sigma_factor
deleted theorem Summable.star
deleted theorem Summable.sub
deleted theorem Summable.subtype
deleted theorem Summable.trans_sub
deleted theorem Summable.tsum_vanishing
deleted theorem Summable.unop
deleted theorem Summable.update
deleted theorem Summable.vanishing
deleted def Summable
deleted theorem hasSum_fintype
deleted theorem hasSum_ite_sub_hasSum
deleted theorem hasSum_nat_add_iff'
deleted theorem hasSum_nat_add_iff
deleted theorem hasSum_op
deleted theorem hasSum_pi_single
deleted theorem hasSum_unop
modified theorem hasSum_zero
deleted theorem rel_iSup_sum
deleted theorem rel_iSup_tsum
deleted theorem rel_sup_add
deleted theorem sum_add_tsum_compl
deleted theorem sum_add_tsum_nat_add'
deleted theorem sum_add_tsum_nat_add
deleted theorem summable_const_iff
deleted theorem summable_iff_vanishing
deleted theorem summable_nat_add_iff
deleted theorem summable_neg_iff
deleted theorem summable_op
deleted theorem summable_star_iff'
deleted theorem summable_star_iff
deleted theorem summable_unop
modified theorem summable_zero
deleted theorem tendsto_sum_nat_add
deleted theorem tsum_apply
deleted theorem tsum_comm'
deleted theorem tsum_comm
deleted theorem tsum_const
deleted theorem tsum_const_smul''
deleted theorem tsum_const_smul'
deleted theorem tsum_const_smul
deleted theorem tsum_eq_add_tsum_ite
deleted theorem tsum_eq_zero_add'
deleted theorem tsum_eq_zero_add
deleted theorem tsum_even_add_odd
deleted theorem tsum_iSup_decode₂
deleted theorem tsum_iUnion_decode₂
deleted theorem tsum_neg
deleted theorem tsum_op
deleted theorem tsum_pi_single
deleted theorem tsum_prod'
deleted theorem tsum_prod
deleted theorem tsum_sigma'
deleted theorem tsum_sigma
deleted theorem tsum_star
deleted theorem tsum_sub
deleted theorem tsum_unop
added theorem HasSum.op
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.tsum_fiberwise
added theorem HasSum.unop
added theorem Pi.hasSum
added theorem Pi.summable
added theorem Summable.ofStar
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.unop
added theorem hasSum_op
added theorem hasSum_pi_single
added theorem hasSum_unop
added theorem summable_op
added theorem summable_star_iff'
added theorem summable_star_iff
added theorem summable_unop
added theorem tsum_apply
added theorem tsum_comm'
added theorem tsum_comm
added theorem tsum_op
added theorem tsum_pi_single
added theorem tsum_prod'
added theorem tsum_prod
added theorem tsum_sigma'
added theorem tsum_sigma
added theorem tsum_star
added theorem tsum_unop
added theorem HasSum.summable
added theorem HasSum.tsum_eq
added theorem HasSum.unique
added def HasSum
added theorem Summable.hasSum
added theorem Summable.hasSum_iff
added def Summable
added theorem hasSum_fintype
added theorem HasSum.neg
added theorem HasSum.sub
added theorem HasSum.update
added theorem Summable.neg
added theorem Summable.of_neg
added theorem Summable.sub
added theorem Summable.subtype
added theorem Summable.trans_sub
added theorem Summable.update
added theorem Summable.vanishing
added theorem hasSum_ite_sub_hasSum
added theorem sum_add_tsum_compl
added theorem summable_const_iff
added theorem summable_iff_vanishing
added theorem summable_neg_iff
added theorem tsum_const
added theorem tsum_eq_add_tsum_ite
added theorem tsum_neg
added theorem tsum_sub
added theorem HasSum.const_smul
modified theorem HasSum.smul_const
added theorem Summable.const_smul
modified theorem Summable.smul_const
added theorem tsum_const_smul''
added theorem tsum_const_smul'
added theorem tsum_const_smul
added theorem HasSum.even_add_odd
added theorem HasSum.int_rec
added theorem HasSum.nonneg_add_neg
added theorem HasSum.sum_range_add
added theorem HasSum.tendsto_sum_nat
added theorem hasSum_nat_add_iff'
added theorem hasSum_nat_add_iff
added theorem rel_iSup_sum
added theorem rel_iSup_tsum
added theorem rel_sup_add
added theorem sum_add_tsum_nat_add'
added theorem sum_add_tsum_nat_add
added theorem summable_nat_add_iff
added theorem tendsto_sum_nat_add
added theorem tsum_eq_zero_add'
added theorem tsum_eq_zero_add
added theorem tsum_even_add_odd
added theorem tsum_iSup_decode₂
added theorem tsum_iUnion_decode₂
modified theorem isLUB_hasSum'
modified theorem cauchySeq_of_summable_dist
modified theorem HasSum.div_const
modified theorem HasSum.mul_left
modified theorem HasSum.mul_right
modified theorem Summable.div_const
modified theorem Summable.mul_left
modified theorem Summable.mul_right
modified theorem hasSum_div_const_iff
modified theorem hasSum_mul_left_iff
modified theorem hasSum_mul_right_iff
modified theorem summable_div_const_iff
modified theorem summable_mul_left_iff
modified theorem summable_mul_right_iff