Theorem Submonoid.IsLocalizationMap.hasUniqueRoots

Modification history

2026-10-18 08:25
Mathlib/GroupTheory/MonoidLocalization/Basic.lean
feat(RingTheory/FractionalIdeal): add HasUniqueRoots instance (#40636) …
Added Submonoid.IsLocalizationMap.hasUniqueRootsView on Github →