Def Submonoid.LocalizationMap.toMonoidWithZeroHom

Modification history

2025-08-22 15:03

Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

chore(MonoidLocalization): get rid of Submonoid.LocalizationWithZeroMap (#27842) …

Added Submonoid.LocalizationMap.toMonoidWithZeroHom View on Github →