Commit 2023-08-18 07:22 be7fa69b

feat: define RegularNormedAlgebra and add the norm on the Unitization (#5742) This constructs a norm on the Unitization 𝕜 A of a (possibly non-unital) normed algebra A, subject to the condition that ContinuousLinearMap.mul 𝕜 A is an isometry. A norm on A satisfying this property is said to be regular so we add the class RegularNormedAlgebra where this construction makes sense. This norm is particularly nice because, among norms on the unitization of a RegularNormedAlgebra, this norm is minimal. Moreover, it is the (necessarily unique) C⋆-norm on the unitization when the norm on A is a C⋆-norm (see #5393)

• depends on: #5741