is_R_or_C): register instances of `cstar_ring` (#10555)

Commit

4 years ago

feat(analysis/normed_space/star and data/complex/is_R_or_C): register instances of `cstar_ring` (#10555) Register instances `cstar_ring ℝ` and `cstar_ring K` when `[is_R_or_C K]`

Author

j-loreaux

Parents

3f7d0cfd

mathlib 599a5118 - feat(analysis/normed_space/star and data/complex/is_R_or_C): register instances of `cstar_ring` (#10555)

mathlib
599a5118 - feat(analysis/normed_space/star and data/complex/is_R_or_C): register instances of `cstar_ring` (#10555)