infinite_sum): add lemmas about continuous linear maps (#5243)

Commit

5 years ago

feat(topology/algebra/infinite_sum): add lemmas about continuous linear maps (#5243) Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Author

dupuisf

Parents

f7301374

mathlib b9689bdc - feat(topology/algebra/infinite_sum): add lemmas about continuous linear maps (#5243)

mathlib
b9689bdc - feat(topology/algebra/infinite_sum): add lemmas about continuous linear maps (#5243)