Theorems · Definition · group theory
FreeMonoid.lift
{α : Type u_1} → {M : Type u_4} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)Equivalence between maps α → M and monoid homomorphisms FreeMonoid α →* M.
- Defined in
- Mathlib.Algebra.FreeMonoid.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 42 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
- Equivstatement · cited by 8,337
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- FreeMonoidstatement and proof · cited by 147
- FreeMonoid.ofproof · cited by 69
- FreeMonoid.toListproof · cited by 33
- FreeMonoid.prodAuxproof · cited by 1
Cited by27
Results whose statement or proof uses this declaration.
- Monoid.CoprodI.liftproof · cited by 21
- Monoid.Coprod.liftproof · cited by 13
- FreeRing.liftproof · cited by 6
- Submonoid.closure_induction_leftproof · cited by 4
- Submonoid.closure_eq_mrangestatement · cited by 3
- FreeAlgebra.equivMonoidAlgebraFreeMonoidproof · cited by 3
- Submonoid.closure_eq_image_prodproof · cited by 2
- FreeMonoid.mrange_liftstatement and proof · cited by 2
- PresentedMonoid.liftstatement and proof · cited by 2
- FreeMonoid.equivWithOneFreeSemigroupproof · cited by 2
- FreeMonoid.lift_applystatement · cited by 1
- FreeMonoid.lift_comp_ofstatement · cited by 1