Commit 2026-10-18 08:25 f0320d93

View on Github →

feat(RingTheory/FractionalIdeal): add HasUniqueRoots instance (#40636)

  • The monoid of fractional ideals with respect to S ≤ R⁰ is the localization of the monoid of ideals of R at the principal ideals generated by an element of S.
  • The target of a localization map of a monoid with unique roots has unique roots.
  • As a consequence, the monoid of fractional ideals has unique roots when the monoid of ideals does. A comment also records that the monoid of ideals of a Dedekind domain has unique roots only once Mathlib.Algebra.GroupWithZero.Torsion is imported. :robot: This PR was extracted from the SKW project by Claude.

Estimated changes