Theorem WithLp.equiv_symm_add

Modification history

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