Commit 2025-05-14 15:37 9b1d9062

View on Github →

feat: the Grothendieck group of a fg monoid is fg (#24896) From Toric

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

added def Localization.mkHom

added theorem Localization.mkHom_surjective

Created Mathlib/GroupTheory/MonoidLocalization/Finite.lean

added theorem Localization.fg