Def EuclideanSpace.single

Modification history

2024-03-21 18:11

Mathlib/Analysis/InnerProductSpace/PiL2.lean

chore(LpSpace): cleanup `Fintype`/`Finite` (#11428) …

Modified EuclideanSpace.single View on Github →

2023-05-29 05:29

Mathlib/Analysis/InnerProductSpace/PiL2.lean

feat: port Analysis.InnerProductSpace.PiL2 (#4420) …

Added EuclideanSpace.single View on Github →