Commit 2022-06-20 09:15 2604c048

feat(number_theory/number_field): add definitions and results about embeddings (#14749) We consider the embeddings of a number field into an algebraic closed field (of char. 0) and prove some results about those. We also prove the number_field instance for adjoint_root of an irreducible polynomial of ℚ[X]. From flt-regular