Theorems · Inductive type · group theory

Monoid.PushoutI.NormalWord.Transversal

{ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} → [inst : (i : ι) → Group (G i)] → [inst_1 : Group H] → ((i : ι) → H →* G i) → Type (max u_1 u_2)

The data we need to pick a normal form for words in the pushout. We need to pick a canonical element of each coset. We also need all the maps in the diagram to be injective

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

45 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

GroupGroup