mathlib

0ead8ee9 - feat(ring_theory/localization): Characterize units in localization at prime ideal (#7519)

feat(ring_theory/localization): Characterize units in localization at prime ideal (#7519) Adds a few lemmas characterizing units and nonunits (elements of the maximal ideal) in the localization at a prime ideal.