Theorem IsLprojection.coe_zero

Modification history

2023-03-23 16:06

Mathlib/Analysis/NormedSpace/MStructure.lean

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

Added IsLprojection.coe_zero View on Github →