Def CommGrp.forget₂CommMonAdj

Modification history

2024-09-10 12:58

Mathlib/Algebra/Category/Grp/Adjunctions.lean

refactor(CategoryTheory/Adjunction): switch to unit-counit definition of adjunction (#16317) …

Modified CommGrp.forget₂CommMonAdj View on Github →

2024-06-20 02:11

Mathlib/Algebra/Category/Grp/Adjunctions.lean

chore: Rename to `Grp` (#3731) …

Added CommGrp.forget₂CommMonAdj View on Github →