Theorems · Definition · group theory

Monoid.CoprodI.NeWord.replaceHead

{ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {i j : ι} → (x : M i) → x ≠ 1 → Monoid.CoprodI.NeWord M i j → Monoid.CoprodI.NeWord M i j

One can replace the first letter in a non-empty reduced word by an element of the same group

Defined in: Mathlib.GroupTheory.CoprodI
Cited by: 4 results in Mathlib
Foundations: Depth 11 from the axioms · uses no axioms
Assumes: Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Monoidstatement and proof · cited by 3,887
Monoid.CoprodI.NeWordstatement and proof · cited by 36
Monoid.CoprodI.NeWord.brecOnproof · cited by 2

Cited by5

Results whose statement or proof uses this declaration.

Monoid.CoprodI.NeWord.mulHeadproof · cited by 4
Monoid.CoprodI.NeWord.mulHead_prodproof · cited by 1
Monoid.CoprodI.NeWord.replaceHead_headstatement and proof · cited by 1
Monoid.CoprodI.NeWord.replaceHead.congr_simpstatement and proof · cited by 0
Monoid.CoprodI.NeWord.replaceHead.eq_defstatement and proof · cited by 0