real_algHom_eq_id_or_conj — Mathlib

English

The real-algebra homomorphisms f: ℂ →ₐ[ℝ] ℂ are exactly the identity or complex conjugation conjugation conjAe.

Русский

ℝ-алгебра-гомоморфизмы f: ℂ →ₐ[ℝ] ℂ — это либо тождественный автоморфизм, либо сопряжение conjAe.

LaTeX

$$$ \forall f: \mathbb{C} \to_{\mathbb{R}} \mathbb{C},\ f = \mathrm{id}_{\mathbb{C}} \lor f = conjAe. $$$

Lean4

/-- The identity and the complex conjugation are the only two `ℝ`-algebra homomorphisms of `ℂ`. -/
theorem real_algHom_eq_id_or_conj (f : ℂ →ₐ[ℝ] ℂ) : f = AlgHom.id ℝ ℂ ∨ f = conjAe :=
  by
  refine (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp ?_ ?_ <;>
    refine fun h => algHom_ext ?_
  exacts [h, conj_I.symm ▸ h]

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