Commit 2023-02-01 07:41 78ac1db3

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.