Commit 2025-03-07 14:33 4c7d24c8

View on Github →

chore: rename Mon_ClassOfRepresentableBy to Mon_Class.ofRepresentableBy (#22686)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Yoneda.lean

added def Mon_Class.ofRepresentableBy

added theorem Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy

deleted def Mon_ClassOfRepresentableBy

deleted theorem Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy

added def yonedaMonObjMon_Class.ofRepresentableBy

deleted def yonedaMonObjMon_ClassOfRepresentableBy