Def LinearIsometryEquiv.piLpCurry

Modification history

2024-08-07 10:57

Mathlib/Analysis/Normed/Lp/PiLp.lean

chore: backports for leanprover/lean4#4814 (part 25) (#15537)

Modified LinearIsometryEquiv.piLpCurry View on Github →

2024-06-13 00:50

Mathlib/Analysis/NormedSpace/PiLp.lean

feat: Define `Pi.orthonormalBasis` (#12242) …

Added LinearIsometryEquiv.piLpCurry View on Github →