Theorem PiLp.coe_symm_continuousLinearEquiv

Modification history

2025-11-20 20:48
Mathlib/Analysis/Normed/Lp/PiLp.lean
feat: ofLp and toLp of a sum (#31353) …
Added PiLp.coe_symm_continuousLinearEquivView on Github →