[Merged by Bors] - feat: port Topology.Algebra.InfiniteSum.Order#2644

urkud wants to merge 5 commits intomasterleanprover-community/mathlib4:masterfrom

port/Topology.Algebra.InfiniteSum.Orderleanprover-community/mathlib4:port/Topology.Algebra.InfiniteSum.OrderCopy head branch name to clipboard