Commit 2023-05-22 19:14 76a03066

View on Github →

feat: port Algebra.Category.GroupWithZero (#3962)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/GroupWithZeroCat.lean

added def GroupWithZeroCat.Iso.mk

added theorem GroupWithZeroCat.coe_comp

added theorem GroupWithZeroCat.coe_id

added theorem GroupWithZeroCat.forget_map

added def GroupWithZeroCat.of

added def GroupWithZeroCat