mathlib

651f93df - feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra (#15869)

feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra (#15869) Define the multiplier algebra of a C⋆-algebra as the algebra (over `𝕜`) of double centralizers, for which we provide the localized notation `𝓜(𝕜, A)`. A double centralizer is a pair of continuous linear maps `L R : A →L[𝕜] A` satisfying the intertwining condition `R x * y = x * L y`. There is a natural embedding `A → 𝓜(𝕜, A)` which sends `a : A` to the continuous linear maps `L R : A →L[𝕜] A` given by left and right multiplication by `a`, and we provide this map as a coercion. In this PR we put all the natural structures on `𝓜(𝕜, A)`, culminating in the fact that it is a unital C⋆-algebra when A is a (unital or non-unital) C⋆-algebra. Co-authored-by: Jon Bannon Co-authored-by: Jon Bannon <jbannon@siena.edu>