[Merged by Bors] - fix(data/complex/basic): ensure algebra ℝ ℂ is computable

[eric-wieser]

Without this complex.ring instance, ring ℂ is found via division_ring.to_ring and field.to_division_ring, and complex.field is non-computable.

The non-computable-ness previously contaminated distrib_mul_action R ℂ and even some properties of finset.sum on complex numbers! To avoid this type of mistake again, we remove noncomputable theory and manually flag the parts we actually expect to be computable.

---

• depends on: [Merged by Bors] - fix(data/real/basic): provide a computable module instance #8164

[sgouezel]

Sorry, but isn't everything about real and complex numbers non-computable already? What are you tring to gain here? (I realize it can sound aggressive, but it's not meant to be, that's a real question).

[eric-wieser]

No, only has_inv, decidable_eq and decidable (<) are noncomputable on the reals. Unfortunately lean often finds the addition starting from the noncomputable field structure, which makes lots of things unnecessarily non-computable.

[sgouezel]

Yes, but what is gained by Lean realizing that addition is computable on the complexes (apart from the fact that you don't need to mark any other stuff as noncomputable)?

[eric-wieser]

The motivation was primarily to avoid having to mark things noncomputable erroneously: especially since the existing shortcut instances for real already handle this correctly in almost all cases.

Is it possible to construct some decidably-equal subtype of the complex numbers though, such as the submonoid containing the cube roots of 1? If so, then you can compute with things like zmod 3 ≃+ multiplicative cbrts_one, which could end up noncomputable simply due to the bundling of the equiv.

Is there any harm in adding the instances in this PR, even if the use-case seems largely academic?

[sgouezel]

I don't think there's any harm. I am not convinced there is a real gain either, globally it's probably +\epsilon so still slightly positive :-)

[Vierkantor]

Since you already have done the work, I see no disadvantage to merging this.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - fix(data/real/basic): provide a computable module instance #8164

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[eric-wieser]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[Vierkantor]

(I didn't do bors d+ yet, because I would have liked to check how things looked after the merge. But everything looks fine, and a lot smaller diff in the end than I was expecting, so no further complaining from me.)

[eric-wieser]

Oh, whoops!