feat(data/complex/exponential): exp_eq_one_iff

Author: ChrisHughes24

src/data/complex/exponential.lean

@@ -840,6 +840,9 @@ lemma exp_injective : function.injective exp :=
   { exact absurd h (ne.symm (ne_of_lt (exp_lt_exp h₁))) }
 end
 
+@[simp] lemma exp_eq_one_iff : exp x = 1 ↔ x = 0 :=
+⟨by rw ← exp_zero; exact λ h, exp_injective h, λ h, by rw [h, exp_zero]⟩
+
 end real
 
 namespace complex
@@ -1052,4 +1055,4 @@ by rw [exp_eq_exp_re_mul_sin_add_cos, exp_eq_exp_re_mul_sin_add_cos y,
 @[simp] lemma abs_exp_of_real (x : ℝ) : abs (exp x) = real.exp x :=
 by rw [← of_real_exp]; exact abs_of_nonneg (le_of_lt (real.exp_pos _))
 
-end complex
+end complex