feat(data/complex/basic): of_real_injective (#10464)

leanprover-community · Nov 26, 2021 · 0b9d332 · 0b9d332
1 parent e742fce
commit 0b9d332
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean
@@ -59,6 +59,9 @@ lemma of_real_def (r : ℝ) : (r : ℂ) = ⟨r, 0⟩ := rfl
 @[simp, norm_cast] theorem of_real_inj {z w : ℝ} : (z : ℂ) = w ↔ z = w :=
 ⟨congr_arg re, congr_arg _⟩
 
+theorem of_real_injective : function.injective (coe : ℝ → ℂ) :=
+λ z w, congr_arg re
+
 instance : can_lift ℂ ℝ :=
 { cond := λ z, z.im = 0,
   coe := coe,