Theorems · Theorem · group theory
Monoid.CoprodI.NeWord.prod_singleton
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x : M i) (hne_one : x ≠ 1),
(Monoid.CoprodI.NeWord.singleton x hne_one).prod = Monoid.CoprodI.of x- Defined in
- Mathlib.GroupTheory.CoprodI
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- mul_oneproof · cited by 3,885
- MonoidHomstatement · cited by 3,629
- Monoid.CoprodIstatement · cited by 52
- Monoid.CoprodI.ofstatement and proof · cited by 45
- Monoid.CoprodI.NeWord.prodstatement · cited by 9
Cited by4
Results whose statement or proof uses this declaration.
- Monoid.CoprodI.lift_word_prod_nontrivial_of_head_cardproof · cited by 1
- Monoid.CoprodI.NeWord.mulHead_prodproof · cited by 1
- Monoid.CoprodI.NeWord.inv_prodproof · cited by 1
- Monoid.CoprodI.lift_word_ping_pongproof · cited by 1