Commit 2023-07-16 14:44 1a646ca7

feat(Topology.Algebra.InfiniteSum): make sure that tsum and sum coincide on fintypes (#5914) Currently, when s is a fintype, it is possible that ∑' x, f x ≠ ∑ x, f x (if the topology of the target space is not separated), as the infinite sum ∑' picks some limit if it exists, but not necessarily the one we prefer. This PR tweaks the definition of infinite sums to make sure that, when a function is finitely supported, the chosen limit for its infinite sum is the (finite) sum of its values. This makes it possible to remove a few separation assumption here and there.