Commit 2025-05-19 07:32 ec3711de
View on Github →chore(Topology/ContinuousMap): remove assumptions (#24985)
ContinuousSMul R C(α, M)
andContinuousConstSMul R C(α, M)
no longer needsLocallyCompactSpace α
.ContinuousLinearMap.compLeftContinuous
is upgraded to a continuous linear map.ContinuousLinearMap.compLeftContinuousCompact
is removed because it is a special case of the newContinuousLinearMap.compLeftContinuous
.- Also added
ContinuousLinearMap.const : M →L[R] C(α, M)
.