Commit 2024-11-04 09:56 15f99d44

View on Github →

feat: presented monoids (#13152) Define presented monoids and their universal property. This requires some additions to free monoids, and GroupTheory/Congruence

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/PresentedMonoid/Basic.lean

added theorem PresentedMonoid.closure_range_of

added theorem PresentedMonoid.ext

added def PresentedMonoid.lift

added theorem PresentedMonoid.lift_of

added def PresentedMonoid.mk

added def PresentedMonoid.of

added theorem PresentedMonoid.surjective_mk

added theorem PresentedMonoid.toMonoid.unique

added def PresentedMonoid