Commit 2023-06-01 16:00 9b438dac
View on Github →feat: port Analysis.NormedSpace.LpEquiv (#4554)
This PR also renames Analysis.NormedSpace.LpSpace
to Analysis.NormedSpace.lpSpace
per this Zulip poll
feat: port Analysis.NormedSpace.LpEquiv (#4554)
This PR also renames Analysis.NormedSpace.LpSpace
to Analysis.NormedSpace.lpSpace
per this Zulip poll