mathlib3

78ac1db3 - feat(number_theory/number_field/embeddings): add infinite_places.eq_iff (#17285)

feat(number_theory/number_field/embeddings): add infinite_places.eq_iff (#17285) This is the proof that two embeddings of a field into `ℂ` define the same (infinite) place iff they are equal or complex conjugate. This PR also contains definitions of complex and real infinite places and some basic results about these. Two lemmas about subfields of `ℂ` are in the new file `topology/instances/complex.lean` but they might belong elsewhere.