Commit 2024-09-27 15:03 b2639cfc

feat(NumberTheory/NumberField): Restricting maps to the ring of integers (#16849) This PR adds definitions of restricting maps to the ring of integers. That is, given a ring homomorphism (resp. ring isomorphism; resp. algebra homomorphism; resp. algebra isomorphism) f fromK to L, we define the induced ring homomorphism (resp. ring isomorphism; resp. algebra homomorphism; resp. algebra isomorphism) from 𝓞 K to 𝓞 L, which is obtained by restricting f to 𝓞 K.