Theorem IsLprojection.le_def

Modification history

2023-03-23 16:06

Mathlib/Analysis/NormedSpace/MStructure.lean

feat: port Analysis.NormedSpace.MStructure (#2915) …

Added IsLprojection.le_def View on Github →