mathlib3

0a375900 - feat(algebra/star/subalgebra): develop some API for `star_subalgebra` (#16896)

feat(algebra/star/subalgebra): develop some API for `star_subalgebra` (#16896) Some of this is necessary to define the (closed) C⋆-algebra generated by a single element, which is in turn necessary to define the continuous functional calculus.