Theorem WithLp.equiv_symm_neg

Modification history

2023-08-14 01:22
Mathlib/Analysis/NormedSpace/WithLp.lean
refactor: generalize PiLp to WithLp (#6409) …
Added WithLp.equiv_symm_negView on Github →