Commit 2021-02-28 01:58 9668bdd5
View on Github →feat(algebra/category/Mon/adjunctions): adjoin_unit adjunction from Semigroup (#6440)
This PR provides the adjoin_unit-forgetful adjunction between Semigroup and Mon and additionally the second to last module doc in algebra, namely algebra.group.with_one.