Theorems · Definition · group theory
AddMonoid.Coprod.inl
{M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M →+ AddMonoid.Coprod M NThe natural embedding M →+ AddMonoid.Coprod M N.
- Defined in
- Mathlib.GroupTheory.Coprod.Basic
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 47 from the axioms · uses propext, Quot.sound
- Assumes
- AddZeroClassAddZeroClass
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.
- DFunLike.coeproof · cited by 62,936
- AddMonoidHomstatement · cited by 3,230
- AddZeroClassstatement and proof · cited by 1,237
- AddMonoid.Coprodstatement · cited by 104
- FreeAddMonoid.ofproof · cited by 69
- AddMonoid.Coprod.mkproof · cited by 16
Cited by45
Results whose statement or proof uses this declaration.
- AddMonoid.Coprod.hom_extstatement and proof · cited by 12
- AddEquiv.coprodAssocproof · cited by 6
- AddMonoid.Coprod.mclosure_range_inl_union_inrstatement and proof · cited by 3
- AddMonoid.Coprod.fst_prod_sndproof · cited by 3
- AddEquiv.coprodPUnitproof · cited by 2
- AddMonoid.Coprod.mrange_inl_sup_mrange_inrstatement and proof · cited by 2
- AddMonoid.Coprod.range_inl_sup_range_inrstatement and proof · cited by 2
- AddMonoid.Coprod.fst_apply_inlstatement · cited by 2
- AddMonoid.Coprod.lift_comp_inlstatement · cited by 1
- AddMonoid.Coprod.mk_of_neg_addproof · cited by 1
- AddMonoid.Coprod.mrange_eqstatement and proof · cited by 1
- AddMonoid.Coprod.range_eqstatement and proof · cited by 1