chore(analysis/complex/circle): upgrade exp_map_circle to `continuo…

…us_map` (#9942)

src/analysis/complex/circle.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import analysis.complex.basic
-import data.complex.exponential
+import analysis.special_functions.exp
+import topology.continuous_function.basic
 
 /-!
 # The circle
@@ -86,16 +86,23 @@ instance : topological_group circle :=
     complex.conj_cle.continuous.comp continuous_subtype_coe }
 
 /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`. -/
-def exp_map_circle (t : ℝ) : circle :=
-⟨exp (t * I), by simp [exp_mul_I, abs_cos_add_sin_mul_I]⟩
+def exp_map_circle : C(ℝ, circle) :=
+{ to_fun := λ t, ⟨exp (t * I), by simp [exp_mul_I, abs_cos_add_sin_mul_I]⟩ }
 
 @[simp] lemma exp_map_circle_apply (t : ℝ) : ↑(exp_map_circle t) = complex.exp (t * complex.I) :=
 rfl
 
+@[simp] lemma exp_map_circle_zero : exp_map_circle 0 = 1 :=
+subtype.ext $ by rw [exp_map_circle_apply, of_real_zero, zero_mul, exp_zero, submonoid.coe_one]
+
+@[simp] lemma exp_map_circle_add (x y : ℝ) :
+  exp_map_circle (x + y) = exp_map_circle x * exp_map_circle y :=
+subtype.ext $ by simp only [exp_map_circle_apply, submonoid.coe_mul, of_real_add, add_mul,
+  complex.exp_add]
+
 /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`, considered as a homomorphism of
 groups. -/
 def exp_map_circle_hom : ℝ →+ (additive circle) :=
-{ to_fun := exp_map_circle,
-  map_zero' := by { rw exp_map_circle, convert of_mul_one, simp },
-  map_add' := λ x y, show exp_map_circle (x + y) = (exp_map_circle x) * (exp_map_circle y),
-    from subtype.ext $ by simp [exp_map_circle, exp_add, add_mul] }
+{ to_fun := additive.of_mul ∘ exp_map_circle,
+  map_zero' := exp_map_circle_zero,
+  map_add' := exp_map_circle_add }