Commit 2022-10-12 16:16 65fbcb33

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