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.

src/data/complex/basic.lean

@@ -139,6 +139,10 @@ by refine_struct { zero := (0 : ℂ), add := (+), neg := has_neg.neg, sub := has
   gsmul := @gsmul_rec _ ⟨(0)⟩ ⟨(+)⟩ ⟨has_neg.neg⟩ };
 intros; try { refl }; apply ext_iff.2; split; simp; {ring1 <|> ring_nf}
 
+/-- This shortcut instance ensures we do not find `ring` via the noncomputable `complex.field`
+instance. -/
+instance : ring ℂ := by apply_instance
+
 instance re.is_add_group_hom : is_add_group_hom complex.re :=
 { map_add := complex.add_re }
 

src/data/complex/module.lean

@@ -33,7 +33,6 @@ It also provides a universal property of the complex numbers `complex.lift`, whi
 `ℂ →ₐ[ℝ] A` into any `ℝ`-algebra `A` given a square root of `-1`.
 
 -/
-noncomputable theory
 
 namespace complex
 
@@ -138,7 +137,7 @@ end
 open submodule finite_dimensional
 
 /-- `ℂ` has a basis over `ℝ` given by `1` and `I`. -/
-def basis_one_I : basis (fin 2) ℝ ℂ :=
+noncomputable def basis_one_I : basis (fin 2) ℝ ℂ :=
 basis.of_equiv_fun
 { to_fun := λ z, ![z.re, z.im],
   inv_fun := λ c, c 0 + c 1 • I,
@@ -267,7 +266,7 @@ This can be used to embed the complex numbers in the `quaternion`s.
 
 This isomorphism is named to match the very similar `zsqrtd.lift`. -/
 @[simps {simp_rhs := tt}]
-noncomputable def lift : {I' : A // I' * I' = -1} ≃ (ℂ →ₐ[ℝ] A) :=
+def lift : {I' : A // I' * I' = -1} ≃ (ℂ →ₐ[ℝ] A) :=
 { to_fun := λ I', lift_aux I' I'.prop,
   inv_fun := λ F, ⟨F I, by rw [←F.map_mul, I_mul_I, alg_hom.map_neg, alg_hom.map_one]⟩,
   left_inv := λ I', subtype.ext $ lift_aux_apply_I I' I'.prop,