Theorems · Definition · category theory
uliftPowersHom
(M : Type u) → [inst : Monoid M] → M ≃ (ULift.{u, 0} (Multiplicative ℕ) →* M)Monoid homomorphisms from ULift (Multiplicative ℕ) are defined by the image
of Multiplicative.ofAdd 1.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement · cited by 3,629
- Multiplicativestatement · cited by 875
- MulEquiv.symmproof · cited by 482
- Equiv.transproof · cited by 337
- MulEquiv.uliftproof · cited by 8
- powersHomproof · cited by 6
- MulEquiv.monoidHomCongrLeftEquivproof · cited by 4
Cited by4
Results whose statement or proof uses this declaration.
- MonCat.coyonedaObjIsoForgetproof · cited by 0
- CommMonCat.coyonedaObjIsoForgetproof · cited by 0
- uliftPowersHom_apply_applystatement and proof · cited by 0
- uliftPowersHom_symm_applystatement and proof · cited by 0