Theorem WithLp.equiv_symm_smul

Modification history

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