mathlib3
3b7e7bd6 - feat(normed_space): controlled_sum_of_mem_closure (#8310)

Commit

4 years ago

feat(normed_space): controlled_sum_of_mem_closure (#8310) From LTE

Author

PatrickMassot

PatrickMassot

Parents

Loading