Theorems · Definition · group theory

PresentedAddMonoid.of

{α : Type u_1} → (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) → α → PresentedAddMonoid rels

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

Defined in

Mathlib.Algebra.PresentedMonoid.Basic

Cited by

5 results in Mathlib

Foundations

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