Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes