feat(data/complex/module): add complex.alg_hom_ext (#8105)

src/data/complex/module.lean

@@ -78,6 +78,28 @@ instance [comm_semiring R] [algebra R ℝ] : algebra R ℂ :=
   commutes' := λ r ⟨xr, xi⟩, by ext; simp [smul_re, smul_im, algebra.commutes],
   ..complex.of_real.comp (algebra_map R ℝ) }
 
+/-- Note that when applied the RHS is further simplified by `complex.of_real_eq_coe`. -/
+@[simp] lemma coe_algebra_map : ⇑(algebra_map ℝ ℂ) = complex.of_real := rfl
+
+section
+variables {A : Type*} [semiring A] [algebra ℝ A]
+
+/-- We need this lemma since `complex.coe_algebra_map` diverts the simp-normal form away from
+`alg_hom.commutes`. -/
+@[simp] lemma _root_.alg_hom.map_coe_real_complex (f : ℂ →ₐ[ℝ] A) (x : ℝ) :
+  f x = algebra_map ℝ A x :=
+f.commutes x
+
+/-- Two `ℝ`-algebra homomorphisms from ℂ are equal if they agree on `complex.I`. -/
+@[ext]
+lemma alg_hom_ext ⦃f g : ℂ →ₐ[ℝ] A⦄ (h : f I = g I) : f = g :=
+begin
+  ext ⟨x, y⟩,
+  simp only [mk_eq_add_mul_I, alg_hom.map_add, alg_hom.map_coe_real_complex, alg_hom.map_mul, h]
+end
+
+end
+
 section
 open_locale complex_order
 
@@ -110,8 +132,6 @@ localized "attribute [instance] complex_ordered_module" in complex_order
 end
 
 
-@[simp] lemma coe_algebra_map : ⇑(algebra_map ℝ ℂ) = complex.of_real := rfl
-
 open submodule finite_dimensional
 
 /-- `ℂ` has a basis over `ℝ` given by `1` and `I`. -/