chore(data/real/basic): split off star instance

[hrmacbeth]

Split the star_ring instance off from data/real/basic into a new file data/real/star, thus reducing the imports of the former.

---

previously:
Also delete the construction ring_equiv_Cauchy of a ring equivalence between ℝ and cau_seq.completion.Cauchy: this adds quite a lot of imports, it could also have been put in a separate file but since it's not used anywhere and I can't really imagine a use case it seems easier just to get rid of it.

[semorrison]

I think I'd prefer keeping ring_equiv_Cauchy (or rather, I'd very happily delete it, but only as an independent PR).

[hrmacbeth]

OK, I've made a more conservative version which leaves ring_equiv_Cauchy (so the only change here is the splitting off of the star instance). I'll make another PR later proposing the deletion of ring_equiv_Cauchy, so that it can be discussed properly.

[eric-wieser]

This feels like a somewhat questionable split to me. Is algebra.star.basic a heavy import? I thought it was just some very basic typeclasses.

[hrmacbeth]

@eric-wieser Did you look at the import tree? algebra.star.basic imports algebra.ring.aut which imports algebra.group_ring_action which imports ring_theory.subring.basic. This is one heavy import of many.

[eric-wieser]

To me it sounds like this is fighting the symptom not the cause:

algebra.star.basic imports algebra.ring.aut

This seems somewhat reasonable, but flipping the direction also seems ok

which imports algebra.group_ring_action

This feels backwards, since ring_hom.apply_distrib_mul_action is handled near the material about distrib_mul_actions.

which imports ring_theory.subring.basic. This is one heavy import of many.

This also seems backwards; all the other action typeclasses are provided long before subobjects are defined!

[eric-wieser]

I've opened #17786 with some of the cleanup I was suggesting; I was meaning to do it at some point anyway.

[hrmacbeth]

I still think it wouldn't hurt to split star out of data/real/basic, but it sounds like you have a strong aesthetic preference to keep it in. I'm ok with this, given

• [Merged by Bors] - refactor(algebra/group_ring_action): split out subobject actions #17786 to remove the subobject import from star
• the cleanup of algebra/ring/equiv which just landed in [Merged by Bors] - chore(algebra/ring/equiv): split out results about big operators #17750
• a further splitting of star to remove the finiteness import (currently there because of a few big-operators lemmas) -- can you do this?

[eric-wieser]

a further splitting of star to remove the finiteness import (currently there because of a few big-operators lemmas) -- can you do this?

I don't know if I'll have time to get back to this; but I'll do my best to get #17786 through CI quickly. Indeed, that adds a big_operators import that was previously implicit, so I agree this is probably a good idea.