Theorem AddCommGrpCat.hom_zsmul

Modification history

2026-01-06 15:16

Mathlib/Algebra/Category/Grp/Preadditive.lean

fix: `zsmul` lemmas that were about `nsmul` instead (#33652) …

Modified AddCommGrpCat.hom_zsmul View on Github →

2025-10-12 18:01

Mathlib/Algebra/Category/Grp/Preadditive.lean

chore: rename `Grp` to `GrpCat` (#30191) …

Added AddCommGrpCat.hom_zsmul View on Github →