mathlib

5f2358c4 - fix(data/complex/basic): ensure `algebra ℝ ℂ` is computable (#8166)

fix(data/complex/basic): ensure `algebra ℝ ℂ` is computable (#8166) 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.