Commit 2020-07-15 11:42 a41a3074

refactor(topology/algebra/infinite_sum): review (#3371)

Rename

• has_sum_unique → has_sum.unique;
• summable.summable_comp_of_injective → summable.comp_injective;
• has_sum_iff_tendsto_nat_of_summable → summable.has_sum_iff_tendsto_nat;
• tsum_eq_has_sum → has_sum.tsum_eq;
• support_comp → support_comp_subset, delete support_comp';

Change arguments

• tsum_eq_tsum_of_ne_zero_bij, has_sum_iff_has_sum_of_ne_zero_bij: use functions from support instead of Π x, f x ≠ 0 → β;

Add

• indicator_compl_add_self_apply, indicator_compl_add_self;
• indicator_self_add_compl_apply, indicator_self_add_compl;
• support_subset_iff, support_subset_iff';
• support_subset_comp;
• support_prod_mk;
• embedding.coe_subtype;