Theorems · Theorem · group theory

Monoid.PushoutI.NormalWord.Pair.normalized

∀ {ι : 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 : ι}
  (self : Monoid.PushoutI.NormalWord.Pair d i) (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ self.tail.toList → g ∈ d.set i_1

All letters in the word are in the transversal.

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

5 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

GroupGroup