mathlib

e5a79a7a - feat(analysis/normed_space/star): introduce C*-algebras (#10145)

feat(analysis/normed_space/star): introduce C*-algebras (#10145) This PR introduces normed star rings/algebras and C*-rings/algebras, as well as a version of `star` bundled as a linear isometric equivalence. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>