Theorems · Definition · group theory

Monoid.CoprodI.Word.equivPair

{ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [DecidableEq ι] → [(i : ι) → DecidableEq (M i)] → (i : ι) → Monoid.CoprodI.Word M ≃ Monoid.CoprodI.Word.Pair M i

The equivalence between words and pairs. Given a word, it decomposes it as a pair by removing the first letter if it comes from M i. Given a pair, it prepends the head to the tail.

Defined in: Mathlib.GroupTheory.CoprodI
Cited by: 18 results in Mathlib
Foundations: Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Monoid DecidableEq DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Equivstatement · cited by 8,337
Monoidstatement and proof · cited by 3,887
Monoid.CoprodI.Wordstatement and proof · cited by 55
Monoid.CoprodI.Word.Pairstatement · cited by 32
Monoid.CoprodI.Word.rconsproof · cited by 10

Cited by20

Results whose statement or proof uses this declaration.

Monoid.PushoutI.NormalWord.equivPairproof · cited by 5
Monoid.CoprodI.Word.of_smul_defstatement · cited by 4
Monoid.CoprodI.Word.rcons_eq_smulproof · cited by 3
Monoid.PushoutI.NormalWord.rconsproof · cited by 3
Monoid.CoprodI.Word.equivPair_symmstatement · cited by 3
Monoid.CoprodI.Word.equivPair_eq_of_fstIdx_nestatement and proof · cited by 2
Monoid.CoprodI.Word.equivPair_headstatement · cited by 2
Monoid.CoprodI.Word.equivPair_tail_eq_inv_smulstatement · cited by 2
Monoid.CoprodI.Word.mem_equivPair_tail_iffstatement · cited by 2
Monoid.PushoutI.NormalWord.cons_eq_smulproof · cited by 1
Monoid.CoprodI.Word.prod_smulproof · cited by 1
Monoid.PushoutI.NormalWord.eq_one_of_smul_normalizedproof · cited by 1