Theorem LinearEquiv.coe_withLpCongr

Modification history

2025-11-25 22:49
Mathlib/Analysis/Normed/Lp/WithLp.lean
feat: add `WithLp.map` and variants (#31667)
Added LinearEquiv.coe_withLpCongrView on Github →