Theorem LinearIsometryEquiv.piLpCurry_apply

Modification history

2024-06-13 00:50
Mathlib/Analysis/NormedSpace/PiLp.lean
feat: Define `Pi.orthonormalBasis` (#12242) …
Added LinearIsometryEquiv.piLpCurry_applyView on Github →