Commit 2026-09-29 15:02 cba67dec

feat: introduce an IsNormableSpace class (#42983) This is relevant to be able to use functions like ContinuousLinearMap.flip on tangent spaces, which are normable but not normed. See Zulip discussion at #Is there code for X? > Pulling back continuous inner product @ 💬 This PR introduces a new typeclass IsNormableSpace 𝕜 E modelled on PolynormableSpace 𝕜 E and establishes basic API. It extends basic bilinear functions (like ContinuousLinearMap.flip or ContinuousLInearMap.bilinearComp) to normable spaces. It also shows that finite-dimensional spaces are normable, as well as spaces of continuous linear maps between normable spaces.