complex is a cstar_ring

Stream: general

[Jireh Loreaux]

@Heather Macbeth and @Frédéric Dupuis I am planning to register an instance of our first C^*-algebra:

instance : cstar_ring ℂ :=
{ norm_star_mul_self := λ z, by simp only [star_def, norm, abs_mul, abs_conj] }

I went to place it in analysis/complex/basic, but because cstar_ring is defined in analysis/normed_space/star, I had to import that, which feels wrong. Thoughts?

[Heather Macbeth]

I think it's ok, myself. The file analysis/normed_space/star is very short and all its imports are already imported to analysis.complex.basic. What do you think, Frédéric?