Commit 2026-03-18 15:36 bf010adb

feat: ContinuousLinearMap.continuous_of_continuous_uncurry (#36776) If a bilinear map E × F → G is jointly continuous, then it defines a continuous linear map E → F → G. In other words, a continuous bilinear map is hypocontinuous. The key argument was essentially already present in ContinuousLinearMap.toSpanSingletonCLE.