Commit 2023-03-26 08:17 ea4e0dd0

View on Github →

feat: port Algebra.Category.GroupCat.Zero (#3092)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/GroupCat/Zero.lean

added theorem CommGroupCat.isZero_of_subsingleton

added theorem GroupCat.isZero_of_subsingleton