Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lp.ext

Modification history

2022-01-01 02:32

src/analysis/normed_space/lp_space.lean

feat(normed_space/lp_space): Lp space for `Π i, E i` (#11015) …

Added lp.ext View on Github →