Commit 2026-02-26 16:02 04289d97

feat: SeparatelyContinuousMul class for multiplication which is continuous in each variable (#35589) In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it is continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets. In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use ContinuousMul. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity is ContinuousConstSMul α α and ContinuousConstSMul αᵐᵒᵖ α, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about • instead of *. Consequently, in this PR we define classes SeparatelyContinuousMul (and SeparatelyContinuousAdd via to_additive) to encode this weaker form of continuity of multiplication.