mathlib3

65fbcb33 - feat(number_theory/number_field): add map_mem_ring_of_integers (#16754)

feat(number_theory/number_field): add map_mem_ring_of_integers (#16754) We add `number_field.map_mem_ring_of_integers`, the image of an element of the ring of integers under `f : K →ₐ[ℚ] L` lies in the ring of integer. In particular, the Galois group preserve the ring of integers. From flt-regular