Commit 2026-01-06 15:16 8c83f639

View on Github →

fix: zsmul lemmas that were about nsmul instead (#33652) Found thanks to Jovan: #mathlib4 > duplicate declarations @ 💬

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Preadditive.lean

modified theorem AddCommGrpCat.hom_zsmul

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

modified theorem ModuleCat.hom_zsmul

Modified Mathlib/Algebra/Category/ModuleCat/Semi.lean

deleted theorem SemimoduleCat.hom_zsmul