mathlib

3419dfc0 - feat(analysis/normed_space/lp_space): construct star structures on lp spaces (#15317)

feat(analysis/normed_space/lp_space): construct star structures on lp spaces (#15317) On general `lp` spaces we construct a star add monoid and star module structure, and in the case when `1 ≤ p` we also show it is a normed star group. In addition, for `p = ∞`, we provide a star ring structure and show that it is a C⋆-ring. This establishes that the (\ell ^ \infty) direct sum of C⋆-algebras is itself a C⋆-algebra with the supremum norm. Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>