Def PiLp

Modification history

2023-08-14 01:22

Mathlib/Analysis/NormedSpace/PiLp.lean

refactor: generalize PiLp to WithLp (#6409) …

Deleted PiLp View on Github →

2023-08-10 19:52

Mathlib/Analysis/NormedSpace/PiLp.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified PiLp View on Github →

2023-05-26 22:04

Mathlib/Analysis/NormedSpace/PiLp.lean

feat: port Analysis.NormedSpace.PiLp (#4345)

Added PiLp View on Github →