Commit 2025-09-10 17:34 79f860c7

View on Github →

feat: compute the essential image of mapMon/mapGrp (#29159) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

deleted def Grp_Class.tensorObj.CategoryTheory.Functor.FullyFaithful.grp_Class

added theorem Grp_Class.tensorObj.CategoryTheory.Functor.essImage_mapGrp

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added theorem CategoryTheory.Functor.essImage_mapMon