mathlib3

77d020f7 - feat(number_theory/number_field.lean): generalise ```range_eq_roots``` to relative extensions (#15903)

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.