Commit 2025-10-28 10:18 e31670e3
View on Github →chore(Analysis/InnerProductSpace/Defs): generalize InnerProductSpace.ofCore to allow for pre-inner product space (#30945)
This allows us to construct a pre-inner product space (i.e., SeminormedAddCommGroup and InnerProductSpace) using PreInnerProductSpace.Core.