2024-12-14 20:37
Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean
feat(Algebra/Category/Grp/ForgetCorepresentable, Algebra/Category/MonCat/ForgetCorepresentable): the forgetful functor on the category of monoids is corepresentable (#19964) …
Added MonCat.coyonedaObjIsoForget