Commit 2022-02-26 23:31 188b371b

View on Github →

feat(algebra/category/GroupWithZero): The category of groups with zero (#12278) Define GroupWithZero, the category of groups with zero with monoid with zero homs.

Estimated changes

Created src/algebra/category/GroupWithZero.lean

added def GroupWithZero.iso.mk

added def GroupWithZero.of

added def GroupWithZero

Modified src/data/equiv/mul_add.lean