Zulip Chat Archive

Stream: general

Topic: complex is a cstar_ring

Jireh Loreaux (Nov 30 2021 at 17:10):

@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 (Nov 30 2021 at 17:13):

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?

Last updated: Aug 03 2023 at 10:10 UTC