Theorems · Definition · category theory
uliftZMultiplesHom
(G : Type u) → [inst : AddGroup G] → G ≃ (ULift.{u, 0} ℤ →+ G)The equivalence (ULift ℤ →+ G) ≃ G for any additive group G.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 43 from the axioms · uses propext, Quot.sound
- Assumes
- AddGroup
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.
- Equivstatement · cited by 8,337
- AddGroupstatement and proof · cited by 4,410
- AddMonoidHomstatement · cited by 3,230
- AddEquiv.symmproof · cited by 530
- Equiv.transproof · cited by 337
- AddEquiv.uliftproof · cited by 16
- zmultiplesHomproof · cited by 7
- AddEquiv.addMonoidHomCongrLeftEquivproof · cited by 4
Cited by7
Results whose statement or proof uses this declaration.
- AddCommGrpCat.uliftZMultiplesAddEquivproof · cited by 3
- uliftZMultiplesHom_apply_applystatement and proof · cited by 1
- AddCommGrpCat.uliftZMultiplesAddEquiv_applystatement · cited by 0
- AddGrpCat.coyonedaObjIsoForgetproof · cited by 0
- uliftZMultiplesHom_apply_addstatement · cited by 0
- uliftZMultiplesHom_symm_applystatement and proof · cited by 0
- AddCommGrpCat.coyonedaObjIsoForgetproof · cited by 0