mathlib

489c1c57 - feat(analysis/complex/basic): add `complex.ring_hom_eq_id_or_conj_of_continuous` (#16169)

feat(analysis/complex/basic): add `complex.ring_hom_eq_id_or_conj_of_continuous` (#16169) We prove that the only continuous ring homorphism from $\mathbb{C}$ to $\mathbb{C}$ are the identity and the complex conjugation. We deduce the result from a first lemma that gives the same conclusion for the $\mathbb{R}$-algebra homomorphisms from $\mathbb{C}$ to $\mathbb{C}$.