feat(data/real/dedekind_cut): define and add_comm_group

[pechersky]

Based on Principles of mathematical analysis by Rudin TODO: finish proving they form a field, and are isomorphic to the reals.

---

[YaelDillies]

Have you seen concept? This is a generalization of Dedekind cuts. Also I think your pointwise lemmas are all abstracted away in #13669 (by showing that Sup preserves addition, multiplication). And finally the "isomorphic to the reals" part will be a direct consequence of #3292.

[pechersky]

Have you seen concept? This is a generalization of Dedekind cuts. Also I think your pointwise lemmas are all abstracted away in #13669 (by showing that Sup preserves addition, multiplication). And finally the "isomorphic to the reals" part will be a direct consequence of #3292.

Would you suggest abandoning this? My goal is to place an "archimedean linear ordered field" instance on this type that I am building. Would we do it instead on concept?

[YaelDillies]

Actually, there is one difference. Namely, Dedekind cuts don't give you ⊥ and ⊤. Still, I think this should wait for #3292 because this is quite literally what it is designed for (the head of the queue is #14307).

[pechersky]

#3292 will allow us to how that cut Q \~- R, but we still need to build that cut Q is archimedean linear field. Am I missing something?

[YaelDillies]

No no, that's right. But your todo is about the isomorphism to the reals, and my point is that you don't actually need to do that part.