mathlib

9668bdd5 - feat(algebra/category/Mon/adjunctions): adjoin_unit adjunction from Semigroup (#6440)

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`.