Theorems · Definition · group theory

PresentedGroup.coprodPresentations

{α : Type u_1} →
  {β : Type u_2} →
    (rels₁ : Set (FreeGroup α)) →
      (rels₂ : Set (FreeGroup β)) →
        PresentedGroup (⇑(FreeGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeGroup.map Sum.inr) '' rels₂) ≃*
          Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)

The free product (Coproduct) of presentations is isomorphic to the presentation of the union over the FreeGroup (α ⊕ β)

Defined in

Mathlib.GroupTheory.PresentedGroup

Cited by

0 results in Mathlib

Foundations

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