Theorems · Definition · group theory
FreeAddSemigroup.toFreeAddMonoid
{α : Type u_1} → FreeAddSemigroup α →ₙ+ FreeAddMonoid αThe natural embedding of the free additive semigroup into the
free additive monoid. This is injective (FreeAddSemigroup.toFreeAddMonoid_injective), and its
image consists of all non-0 elements of the free additive monoid
(FreeAddSemigroup.eq_zero_or_toFreeAddMonoid).
- Defined in
- Mathlib.Algebra.FreeMonoid.FreeSemigroup
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 39 from the axioms · uses propext, Quot.sound
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
- AddHomstatement · cited by 294
- FreeAddMonoidstatement · cited by 145
- FreeAddMonoid.ofproof · cited by 69
- FreeAddSemigroupstatement · cited by 43
- FreeAddSemigroup.liftproof · cited by 8
Cited by8
Results whose statement or proof uses this declaration.
- FreeAddMonoid.equivWithZeroFreeAddSemigroupproof · cited by 2
- FreeAddSemigroup.toFreeAddMonoid_mk_eq_consstatement · cited by 1
- FreeAddSemigroup.toFreeAddMonoid_ne_zerostatement and proof · cited by 1
- FreeAddSemigroup.range_toFreeAddMonoidstatement · cited by 0
- FreeAddSemigroup.toFreeAddMonoid_injectivestatement and proof · cited by 0
- FreeAddSemigroup.toFreeAddMonoid_ofstatement · cited by 0
- FreeAddMonoid.equivWithZeroFreeAddSemigroup_symm_applystatement · cited by 0
- FreeAddSemigroup.eq_zero_or_toFreeAddMonoidstatement and proof · cited by 0