Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes