Def yonedaMonObjMon_ClassOfRepresentableBy

Modification history

2025-03-07 14:33
Mathlib/CategoryTheory/Monoidal/Yoneda.lean
chore: rename Mon_ClassOfRepresentableBy to Mon_Class.ofRepresentableBy (#22686)
Deleted yonedaMonObjMon_ClassOfRepresentableByView on Github →
2025-02-15 21:17
Mathlib/CategoryTheory/Monoidal/Yoneda.lean
feat(CategoryTheory/Monoidal): yoneda embedding of `Mon_ C` (#21394)
Added yonedaMonObjMon_ClassOfRepresentableByView on Github →