Commit 2024-05-26 19:45 cee9bb22

feat: norm structure on WithLp 1 (Unitization 𝕜 A) (#12582) Unitization 𝕜 A is equipped with a norm when A is a RegularNormedAlgebra, and it turns out that norm is minimal among all norms for which the natural coercion from A is an isometry and which satisfy ‖1‖ = 1. There is also a maximal norm, given by ‖x‖ := ‖x.fst‖ + ‖x.snd‖, and this norm also makes sense even when A is not a RegularNormedAlgebra. We place this norm on the type synonym WithLp 1 (Unitization 𝕜 A).