Commit 2021-02-26 07:13 24ed74a2

View on Github →

feat(algebra/category/Semigroup/basic): categories of magmas and semigroups (#6387) This PR introduces the category of magmas and the category of semigroups, together with their additive versions.

Estimated changes

Modified src/algebra/category/Mon/basic.lean

deleted theorem mul_equiv.to_CommMon_iso_hom

deleted theorem mul_equiv.to_CommMon_iso_inv

deleted theorem mul_equiv.to_Mon_iso_hom

deleted theorem mul_equiv.to_Mon_iso_inv

Created src/algebra/category/Semigroup/basic.lean

added theorem Magma.coe_of

added def Magma.of

added def Magma

added theorem Semigroup.coe_of

added def Semigroup.of

added def Semigroup

added def category_theory.iso.Magma_iso_to_mul_equiv

added def category_theory.iso.Semigroup_iso_to_mul_equiv

added def mul_equiv.to_Magma_iso

added def mul_equiv.to_Semigroup_iso

added def mul_equiv_iso_Magma_iso

added def mul_equiv_iso_Semigroup_iso

Created src/algebra/pempty_instances.lean