refactor(analysis/special_functions): generalise nth-root lemmas (#9704)

`exists_pow_nat_eq` and `exists_eq_mul_self` both hold for any algebraically closed field, so pull them out into `is_alg_closed/basic` and generalise appropriately

Closes #4674

src/analysis/special_functions/complex/log.lean

@@ -71,21 +71,6 @@ lemma log_I : log I = π / 2 * I := by simp [log]
 
 lemma log_neg_I : log (-I) = -(π / 2) * I := by simp [log]
 
-lemma exists_pow_nat_eq (x : ℂ) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x :=
-begin
-  by_cases hx : x = 0,
-  { use 0, simp only [hx, zero_pow_eq_zero, hn] },
-  { use exp (log x / n),
-    rw [← exp_nat_mul, mul_div_cancel', exp_log hx],
-    exact_mod_cast (pos_iff_ne_zero.mp hn) }
-end
-
-lemma exists_eq_mul_self (x : ℂ) : ∃ z, x = z * z :=
-begin
-  obtain ⟨z, rfl⟩ := exists_pow_nat_eq x zero_lt_two,
-  exact ⟨z, sq z⟩
-end
-
 lemma two_pi_I_ne_zero : (2 * π * I : ℂ) ≠ 0 :=
 by norm_num [real.pi_ne_zero, I_ne_zero]
 

src/analysis/special_functions/trigonometric/complex.lean

@@ -5,6 +5,8 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin
 -/
 import algebra.quadratic_discriminant
 import analysis.special_functions.complex.log
+import analysis.complex.polynomial
+import field_theory.is_alg_closed.basic
 
 /-!
 # Complex trigonometric functions
@@ -204,7 +206,8 @@ lemma cos_surjective : function.surjective cos :=
 begin
   intro x,
   obtain ⟨w, w₀, hw⟩ : ∃ w ≠ 0, 1 * w * w + (-2 * x) * w + 1 = 0,
-  { rcases exists_quadratic_eq_zero (@one_ne_zero ℂ _ _) (exists_eq_mul_self _) with ⟨w, hw⟩,
+  { rcases exists_quadratic_eq_zero (@one_ne_zero ℂ _ _) (is_alg_closed.exists_eq_mul_self _)
+      with ⟨w, hw⟩,
     refine ⟨w, _, hw⟩,
     rintro rfl,
     simpa only [zero_add, one_ne_zero, mul_zero] using hw },

src/field_theory/is_alg_closed/basic.lean

@@ -70,6 +70,22 @@ variables {k}
 theorem exists_root [is_alg_closed k] (p : polynomial k) (hp : p.degree ≠ 0) : ∃ x, is_root p x :=
 exists_root_of_splits _ (is_alg_closed.splits p) hp
 
+lemma exists_pow_nat_eq [is_alg_closed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x :=
+begin
+  rcases exists_root (X ^ n - C x) _ with ⟨z, hz⟩, swap,
+  { rw degree_X_pow_sub_C hn x,
+    exact ne_of_gt (with_bot.coe_lt_coe.2 hn) },
+  use z,
+  simp only [eval_C, eval_X, eval_pow, eval_sub, is_root.def] at hz,
+  exact sub_eq_zero.1 hz
+end
+
+lemma exists_eq_mul_self [is_alg_closed k] (x : k) : ∃ z, x = z * z :=
+begin
+  rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩,
+  exact ⟨z, sq z⟩
+end
+
 theorem exists_eval₂_eq_zero_of_injective {R : Type*} [ring R] [is_alg_closed k] (f : R →+* k)
   (hf : function.injective f) (p : polynomial R) (hp : p.degree ≠ 0) : ∃ x, p.eval₂ f x = 0 :=
 let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective hf]) in