Commit 2023-06-06 12:49 41086ad7

View on Github →

feat: port RingTheory.Localization.Away.AdjoinRoot (#4725)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem AdjoinRoot.root_isInv

deleted theorem AdjoinRoot.root_is_inv

Created Mathlib/RingTheory/Localization/Away/AdjoinRoot.lean

added theorem IsLocalization.Away.finitePresentation

added theorem IsLocalization.adjoin_inv