feat(analysis/complex/circle): exp_map_circle_neg (#11889)

Add the lemma `exp_map_circle_neg`, similar to other lemmas for `exp_map_circle` that are already present.
leanprover-community · Feb 7, 2022 · 2364a09 · 2364a09
1 parent 99215e3
commit 2364a09
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/analysis/complex/circle.lean b/src/analysis/complex/circle.lean
@@ -122,3 +122,6 @@ def exp_map_circle_hom : ℝ →+ (additive circle) :=
 @[simp] lemma exp_map_circle_sub (x y : ℝ) :
   exp_map_circle (x - y) = exp_map_circle x / exp_map_circle y :=
 exp_map_circle_hom.map_sub x y
+
+@[simp] lemma exp_map_circle_neg (x : ℝ) : exp_map_circle (-x) = (exp_map_circle x)⁻¹ :=
+exp_map_circle_hom.map_neg x