Commit 2021-05-11 18:00 3048d6bc
View on Github →feat(ring_theory/localization): Define local ring hom on localization at prime ideal (#7522) Defines the induced ring homomorphism on the localizations at a prime ideal and proves that it is local and uniquely determined.