Commit 2022-08-09 19:12 77d020f7

feat(number_theory/number_field.lean): generalise range_eq_roots to relative extensions (#15903) The statement of range_eq_roots is generalised to relative extensions: Let A be an algebraically closed field and let x ∈ K, with K a number field. For F, subfield of K, the images of x by the F-algebra morphisms from K to A are exactly the roots in A of the minimal polynomial of x over F. The original version over ℚ is a direct consequence. Still, I kept the statement since I think it is useful.