Commit 2026-04-27 12:44 9087ffda

View on Github →

chore(CategoryTheory/Monoidal): rename Mod_ to Mod (#38342) We also rename IsMod_Hom to IsModHom. This is analogous to the previous renames for Mon and Grp.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean

added def CategoryTheory.Mod.trivialAction

deleted def CategoryTheory.Mod_.trivialAction

Modified Mathlib/CategoryTheory/Monoidal/Mod_.lean

added def CategoryTheory.Mod.Hom.mk''

added def CategoryTheory.Mod.Hom.mk'

added structure CategoryTheory.Mod.Hom

added theorem CategoryTheory.Mod.assoc_flip

added def CategoryTheory.Mod.comap

added def CategoryTheory.Mod.comp

added theorem CategoryTheory.Mod.comp_hom'

added def CategoryTheory.Mod.forget

added theorem CategoryTheory.Mod.hom_ext

added def CategoryTheory.Mod.id

added theorem CategoryTheory.Mod.id_hom'

added def CategoryTheory.Mod.regular

added def CategoryTheory.Mod.scalarRestriction

added theorem CategoryTheory.Mod.scalarRestriction_hom

added structure CategoryTheory.Mod

deleted theorem CategoryTheory.ModObj.mul_smul

deleted theorem CategoryTheory.ModObj.one_smul

deleted def CategoryTheory.Mod_.Hom.mk''

deleted def CategoryTheory.Mod_.Hom.mk'

deleted structure CategoryTheory.Mod_.Hom

deleted theorem CategoryTheory.Mod_.assoc_flip

deleted def CategoryTheory.Mod_.comap

deleted def CategoryTheory.Mod_.comp

deleted theorem CategoryTheory.Mod_.comp_hom'

deleted def CategoryTheory.Mod_.forget

deleted theorem CategoryTheory.Mod_.hom_ext

deleted def CategoryTheory.Mod_.id

deleted theorem CategoryTheory.Mod_.id_hom'

deleted def CategoryTheory.Mod_.regular

deleted def CategoryTheory.Mod_.scalarRestriction

deleted theorem CategoryTheory.Mod_.scalarRestriction_hom

deleted structure CategoryTheory.Mod_