Theorems · Theorem · group theory

Monoid.PushoutI.NormalWord.eq_one_of_smul_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 φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (w : Monoid.CoprodI.Word G) {i : ι} (h : H),
  (∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) →
    (∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (Monoid.CoprodI.of ((φ i) h) • w).toList → g ∈ d.set j) → h = 1

Given a word in CoprodI, if every letter is in the transversal and when we multiply by an element of the base group it still has this property, then the element of the base group we multiplied by was one.

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupDecidableEqDecidableEq