Commit 2021-05-07 04:59 0ead8ee9
View on Github →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.