Structure WithLp

Modification history

2025-11-25 22:49

Mathlib/Analysis/Normed/Lp/WithLp.lean

feat: add `WithLp.map` and variants (#31667)

Modified WithLp View on Github →

2025-11-05 17:51

Mathlib/Analysis/Normed/Lp/WithLp.lean

chore: turn WithLp into a structure (#27270) …

Added WithLp View on Github →