Def WithLp.unitizationAlgEquiv

Modification history

2024-05-26 19:45
Mathlib/Analysis/NormedSpace/UnitizationL1.lean
feat: norm structure on `WithLp 1 (Unitization 𝕜 A)` (#12582) …
Added WithLp.unitizationAlgEquivView on Github →