Commit 2023-05-10 01:01 70f423bd

View on Github →

feat: port Algebra.Category.Group.EquivalenceGroupAddGroup (#3861)

Estimated changes

Modified Mathlib.lean

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

added def AddCommGroupCat.toCommGroupCat

added def AddGroupCat.toGroupCat

added def CommGroupCat.toAddCommGroupCat

added def GroupCat.toAddGroupCat

added def commGroupAddCommGroupEquivalence

added def groupAddGroupEquivalence