Theorems · Definition · group theory
Monoid.CoprodI.of
{ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i : ι} → M i →* Monoid.CoprodI MThe inclusion of a summand into the free product.
- Defined in
- Mathlib.GroupTheory.CoprodI
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement · cited by 3,629
- FreeMonoid.ofproof · cited by 69
- Monoid.CoprodIstatement · cited by 52
- conGenproof · cited by 23
- Con.mk'proof · cited by 22
- Monoid.CoprodI.Relproof · cited by 3
Cited by52
Results whose statement or proof uses this declaration.
- Monoid.CoprodI.liftproof · cited by 21
- Monoid.PushoutI.ofproof · cited by 20
- Monoid.CoprodI.Word.prodproof · cited by 11
- Monoid.CoprodI.lift_ofstatement · cited by 8
- Monoid.PushoutI.NormalWord.equivPairproof · cited by 5
- Monoid.CoprodI.NeWord.prod_singletonstatement and proof · cited by 4
- Monoid.CoprodI.Word.of_smul_defstatement · cited by 4
- Monoid.CoprodI.NeWord.append_prodproof · cited by 4
- Monoid.PushoutI.ofCoprodI_ofstatement · cited by 4
- Monoid.PushoutI.of_comp_eq_baseproof · cited by 3
- Monoid.CoprodI.induction_onstatement and proof · cited by 3
- Monoid.CoprodI.Word.rcons_eq_smulstatement · cited by 3