Theorems · Definition · group theory

PresentedGroup.of

{α : Type u_1} → {rels : Set (FreeGroup α)} → α → PresentedGroup rels

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

Defined in

Mathlib.GroupTheory.PresentedGroup

Cited by

12 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound