Commit 2023-07-01 05:24 727956d2

View on Github →

feat: port Algebra.Category.Semigroup.Basic (#4857)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Created Mathlib/Algebra/Category/SemigroupCat/Basic.lean

added def CategoryTheory.Iso.magmaCatIsoToMulEquiv

added def CategoryTheory.Iso.semigroupCatIsoToMulEquiv

added theorem MagmaCat.MulEquiv_coe_eq

added theorem MagmaCat.coe_of

added def MagmaCat.of

added def MagmaCat.ofHom

added theorem MagmaCat.ofHom_apply

added def MagmaCat

added def MulEquiv.toMagmaCatIso

added def MulEquiv.toSemigroupCatIso

added theorem SemigroupCat.MulEquiv_coe_eq

added theorem SemigroupCat.coe_of

added def SemigroupCat.of

added def SemigroupCat.ofHom

added theorem SemigroupCat.ofHom_apply

added def SemigroupCat

added def mulEquivIsoMagmaIso

added def mulEquivIsoSemigroupCatIso