Commit 2026-03-26 18:37 d6820840

feat: add IsSemitopologicalRing (#36617) With the recent addition of the class SeparatelyContinuousMul, it becomes possible to define IsSemitopologicalRing (and a version for semirings). A semitopological ring is a ring with jointly continuous addition and separately continuous multiplication (and continuous negation, but this is implied by the other two). Such structures arise quite frequently in functional analysis. This PR defines these classes and then generalizes a number of things in the library. For example, the topological closures of ring-like structures only need multiplication to be separately continuous (they also only need addition to be separately continuous, but ring-like structures for which addition is separately but not jointly continuous do not generally arise in practice). In addition, this allows us to weaken the conditions of instances pertaining to ContinuousMap.UniqueHom and ContinuousMapZero.UniqueHom which are used in the continuous functional calculus.