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.

Estimated changes