Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 15:30 7848f28d

View on Github →

feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562) Verifying that internal monoid objects in Type are the same thing as bundled monoid objects.

Estimated changes

added theorem Mod.assoc_flip
added def Mod.comap
added def Mod.comp
added theorem Mod.comp_hom'
added structure Mod.hom
added def Mod.id
added theorem Mod.id_hom'
added def Mod.regular
added structure Mod
added theorem Mon_.assoc_flip
added def Mon_.comp
added theorem Mon_.comp_hom'
added def Mon_.forget
added structure Mon_.hom
added def Mon_.id
added theorem Mon_.id_hom'
added structure Mon_
added theorem punit.ext
added theorem unit.ext
deleted theorem unit.ext