Theorems · Definition · group theory

PresentedMonoid.of

{α : Type u_1} → (rels : FreeMonoid α → FreeMonoid α → Prop) → α → PresentedMonoid rels

of is the canonical map from α to a presented monoid with generators x : α. The term x is mapped to the equivalence class of the image of x in FreeMonoid α.

Defined in

Mathlib.Algebra.PresentedMonoid.Basic

Cited by

5 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound