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

Estimated changes

added def AddEquiv.lpPiLp
added def Equiv.lpPiLp
added theorem Memℓp.all
added theorem coe_addEquiv_lpBcf
added theorem coe_addEquiv_lpPiLp
added theorem coe_algEquiv_lpBcf
added theorem coe_equiv_lpPiLp
added theorem coe_equiv_lpPiLp_symm
added theorem coe_lpBcfₗᵢ
added theorem coe_lpBcfₗᵢ_symm
added theorem coe_lpPiLpₗᵢ
added theorem coe_lpPiLpₗᵢ_symm
added theorem coe_ringEquiv_lpBcf
added theorem equiv_lpPiLp_norm