Theorems · Inductive type · group theory

Monoid.PushoutI.NormalWord.Pair

{ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} → Monoid.PushoutI.NormalWord.Transversal φ → ι → Type (max u_1 u_2)

A Pair d i is a word in the coproduct, Coprod G, the tail, and an element of the group G i, the head. The first letter of the tail must not be an element of G i. Note that the head may be 1. Every letter in the tail must be in the transversal given by d. Similar to Monoid.CoprodI.Pair except every letter must be in the transversal (not including the head letter).

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

9 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

GroupGroup