Theorem LinearIsometryEquiv.piLpCurry_symm_apply

Modification history

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