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.

Estimated changes