Def InnerProductSpace.Core.toSeminormedSpace

Modification history

2024-12-20 05:04

Mathlib/Analysis/InnerProductSpace/Basic.lean

chore(Analysis/InnerProductSpace): split large file (#20046) …

Modified InnerProductSpace.Core.toSeminormedSpace View on Github →

2024-08-07 01:32

Mathlib/Analysis/InnerProductSpace/Basic.lean

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

Added InnerProductSpace.Core.toSeminormedSpace View on Github →