Commit 2021-07-07 17:46 5f2358c4

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.