Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-30 11:06
7f6d00dd
View on Github →
feat: pullback monoid objects along a fully faithful functor (
#29099
) From Toric
Estimated changes
Modified
Mathlib/CategoryTheory/Monoidal/Grp_.lean
added
def
CategoryTheory.Functor.FullyFaithful.grp_Class
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.lean