Commit 2023-02-03 21:38 ff6bde6f

feat(number_theory/number_field/embeddings): add card_complex_embeddings (#17753) Define complex and real places of a number field $K$ and prove that the number of real places is $r_1$ and the number of complex places is $r_2$ where $(r_1, r_2)$ is the signature of $K$.