Theorems · Definition · group theory

PresentedGroup.toCoprod

{α : Type u_1} →
  {β : Type u_2} →
    (rels₁ : Set (FreeGroup α)) →
      (rels₂ : Set (FreeGroup β)) → α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)

The canonical inclusion map from the disjoint union of types to the free product of the relations

Defined in

Mathlib.GroupTheory.PresentedGroup

Cited by

3 results in Mathlib

Foundations

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