Def PreInnerProductSpace.toCore

Modification history

2024-08-07 01:32

Mathlib/Analysis/InnerProductSpace/Basic.lean

feat(Analysis/InnerProductSpace/Basic): add PreInnerProductSpace (#14024) …

Added PreInnerProductSpace.toCore View on Github →