Commit 2023-04-06 10:22 60da01b4

feat(number_theory/number_field/canonical_embedding): add canonical embedding (#17783) This PR defines the canonical embedding of a number field $K$ of signature $(r_1, r_2)$ into $\mathbb{R}^{r_1} × \mathbb{C}^{r_2}$ and prove various results about this embedding, including the fact that the image of the ring of integers of $K$ is discrete.