Commit 2023-11-13 06:59 6eb9f7b3
View on Github →chore(InfiniteSum): use dot notation (#8358)
Rename
summable_of_norm_bounded
->Summable.of_norm_bounded
;summable_of_norm_bounded_eventually
->Summable.of_norm_bounded_eventually
;summable_of_nnnorm_bounded
->Summable.of_nnnorm_bounded
;summable_of_summable_norm
->Summable.of_norm
;summable_of_summable_nnnorm
->Summable.of_nnnorm
;
New lemmas
Summable.of_norm_bounded_eventually_nat
Summable.norm
Misc changes
- Golf a few proofs.