Commit 2025-11-25 22:49 517852ab

View on Github →

feat: add WithLp.map and variants (#31667)

Estimated changes

Modified Mathlib/Analysis/Normed/Lp/WithLp.lean

added theorem LinearEquiv.coe_withLpCongr

added def LinearEquiv.withLpCongr

added theorem LinearEquiv.withLpCongr_refl

added theorem LinearEquiv.withLpCongr_symm

added theorem LinearEquiv.withLpCongr_trans

added theorem LinearMap.coe_withLpMap

added def LinearMap.withLpMap

added theorem LinearMap.withLpMap_comp

added theorem LinearMap.withLpMap_id

added theorem WithLp.coe_congr

added theorem WithLp.congr_refl

added theorem WithLp.congr_symm

added theorem WithLp.congr_trans

added theorem WithLp.map_comp

added theorem WithLp.map_id

modified structure WithLp