Mathlib Map

Theorems · Definition · group theory

Monoid.CoprodI.NeWord.head

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

The first letter of a NeWord

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

Around this declaration

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

Monoid.CoprodI.NeWord.mulHead · cited by 4NeWord.mulHeadMonoid.CoprodI.NeWord.mulHead_prod · cited by 1NeWord.mulHead_prodMonoid.CoprodI.NeWord.of_word · cited by 1NeWord.of_wordMonoid.CoprodI.NeWord.replaceHead_head · cited by 1NeWord.replaceHead_headMonoid.CoprodI.NeWord.toList_head? · cited by 1NeWord.toList_head?Monoid.CoprodI.lift_word_prod_nontrivial_of_head_card · cited by 1CoprodI.lift_word_prod_no…Monoid.CoprodI.NeWord.mulHead_head · cited by 0NeWord.mulHead_headMonoid.CoprodI.NeWord.singleton_head · cited by 0NeWord.singleton_headMonoid.CoprodI.NeWord.head.eq_def · cited by 0head.eq_defMonoid.CoprodI.NeWord.mulHead.congr_simp · cited by 0mulHead.congr_simpMonoid.CoprodI.NeWord.append_head · cited by 0NeWord.append_headMonoid.CoprodI.NeWord.inv_head · cited by 0NeWord.inv_headMonoid.CoprodI.NeWord.inv_last · cited by 0NeWord.inv_lastMonoid · cited by 3887MonoidMonoid.CoprodI.NeWord · cited by 36CoprodI.NeWordMonoid.CoprodI.NeWord.brecOn · cited by 2NeWord.brecOnNeWord.headCITED BYCITES

Cites3

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

Cited by13

Results whose statement or proof uses this declaration.