mathlib3

2604c048 - feat(number_theory/number_field): add definitions and results about embeddings (#14749)

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