algHom_ext — Mathlib

English

Two ℝ-algebra homomorphisms from ℂ to A are equal if they agree on I (the imaginary unit).

Русский

Два ℝ-алгебра-гомоморфа от ℂ в A равны, если их значения на I совпадают.

LaTeX

$$$\\\\forall f,g:\\\\mathbb{C} \\\\to_{\\\\mathbb{R}} A\\\\, (f I = g I) \\\\Rightarrow f = g$$$

Lean4

/-- Two `ℝ`-algebra homomorphisms from `ℂ` are equal if they agree on `Complex.I`. -/
@[ext]
theorem algHom_ext ⦃f g : ℂ →ₐ[ℝ] A⦄ (h : f I = g I) : f = g :=
  by
  ext ⟨x, y⟩
  simp only [mk_eq_add_mul_I, map_add, AlgHom.map_coe_real_complex, map_mul, h]

Похожие утверждения