mathlib

73e45c62 - chore(analysis/normed_space/star): create new folder for normed star rings (#11732)

chore(analysis/normed_space/star): create new folder for normed star rings (#11732) This PR moves the file `analysis/normed_space/star.lean` to the new folder `analysis/normed_space/star` (where it of course becomes `basic.lean`). I expect a lot of material about C*-algebras to land in this folder in the (hopefully) near future.