mathlib

51c6beb4 - feat(number_theory/number_field/embeddings) : add infinite_places (#17844)

feat(number_theory/number_field/embeddings) : add infinite_places (#17844) This PR adds definitions and basic lemmas about places, complex embeddings and infinite places of number field.