Theorems · Theorem · group theory

Monoid.PushoutI.NormalWord.cons_head

∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i)
  (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range),
  (Monoid.PushoutI.NormalWord.cons g w hmw hgr).head = (MonoidHom.ofInjective ⋯).symm (⋯.equiv (g * (φ i) w.head)).1

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupGroup