Theorem WithLp.unitization_nnnorm_def

Modification history

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