Theorems · Definition · group theory
Monoid.Coprod.mk
{M : Type u_1} →
{N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → FreeMonoid (M ⊕ N) →* Monoid.Coprod M NThe natural projection FreeMonoid (M ⊕ N) →* M ∗ N.
- Defined in
- Mathlib.GroupTheory.Coprod.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 44 from the axioms · uses propext, Quot.sound
- Assumes
- MulOneClassMulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MonoidHomstatement · cited by 3,629
- MulOneClassstatement and proof · cited by 1,018
- FreeMonoidstatement · cited by 147
- Monoid.Coprodstatement · cited by 109
- Con.mk'proof · cited by 22
- Monoid.coprodConproof · cited by 3
Cited by20
Results whose statement or proof uses this declaration.
- Monoid.Coprod.inlproof · cited by 48
- Monoid.Coprod.inrproof · cited by 47
- Monoid.Coprod.swapproof · cited by 25
- Monoid.Coprod.mapproof · cited by 12
- Monoid.Coprod.mclosure_range_inl_union_inrproof · cited by 3
- Monoid.Coprod.induction_on'proof · cited by 1
- Monoid.Coprod.mk_eq_mkstatement · cited by 1
- Monoid.Coprod.mk_of_inv_mulstatement and proof · cited by 1
- Monoid.Coprod.mk_surjectivestatement · cited by 1
- Monoid.Coprod.mrange_mkstatement · cited by 1
- Monoid.Coprod.con_inv_mul_cancelproof · cited by 0
- Monoid.Coprod.con_ker_mkstatement · cited by 0