Commit 2026-09-01 18:09 962979ee

feat(Topology/InfiniteSum): applying the sum of functions (#42829) These three one-liners are provided mostly for discoverability. Especially for tsum_apply: when one search for lemma in this shape, they will find the version for pi topology, which is not applicable for function spaces with other topology (e.g. ContinuousLinearMap). This PR comes with a breaking change: the original tprod_apply theorem is now moved to the Pi namespace, alone with existing Pi.hasProd and Pi.multipliable. The new tprod_apply is stated for all suitable FunLike objects.