Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-02 01:48 33085c97

View on Github →

chore(category_theory/monoidal/Mod): rename to Mod_ to avoid name clash in mathlib4 (#18911) This matches the existing Mon_.

Estimated changes

deleted theorem Mod.assoc_flip
deleted def Mod.comap
deleted def Mod.comp
deleted theorem Mod.comp_hom'
deleted def Mod.forget
deleted structure Mod.hom
deleted def Mod.id
deleted theorem Mod.id_hom'
deleted def Mod.regular
deleted structure Mod
added theorem Mod_.assoc_flip
added def Mod_.comap
added def Mod_.comp
added theorem Mod_.comp_hom'
added def Mod_.forget
added structure Mod_.hom
added def Mod_.id
added theorem Mod_.id_hom'
added def Mod_.regular
added structure Mod_