mathlib3

60da01b4 - feat(number_theory/number_field/canonical_embedding): add canonical embedding (#17783)

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. Co-authored-by: Alex J Best <alex.j.best@gmail.com> Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>