Theorem PiLp.equiv_sub

Modification history

2023-08-14 01:22

Mathlib/Analysis/NormedSpace/PiLp.lean

refactor: generalize PiLp to WithLp (#6409) …

Deleted PiLp.equiv_sub View on Github →

2023-05-26 22:04

Mathlib/Analysis/NormedSpace/PiLp.lean

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

Added PiLp.equiv_sub View on Github →