Mathlib Map

Theorems · Definition

AddEquiv.ulift

{α : Type u} → [inst : Add α] → ULift.{u_1, u} α ≃+ α

The additive equivalence between ULift α and α.

Defined in
Mathlib.Algebra.Group.ULift
Cited by
16 results in Mathlib
Foundations
Depth 12 from the axioms · uses no axioms
Assumes
Add
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ULift.moduleEquiv · cited by 18ULift.moduleEquivAddCommGrpCat.uliftFunctor · cited by 7AddCommGrpCat.uliftFunctoruliftZMultiplesHom · cited by 4uliftZMultiplesHomAddGrpCat.uliftFunctor · cited by 2AddGrpCat.uliftFunctorAddMonCat.uliftFunctor · cited by 2AddMonCat.uliftFunctoruliftMultiplesHom · cited by 2uliftMultiplesHomCategoryTheory.Adjunction.compPreadditiveYonedaIso · cited by 2Adjunction.compPreadditiv…AddCommMonCat.uliftFunctor · cited by 2AddCommMonCat.uliftFunctorAddCommGrpCat.isColimit_iff_bijective_desc · cited by 1AddCommGrpCat.isColimit_i…uliftZMultiplesHom_apply_apply · cited by 1uliftZMultiplesHom_apply_…AddCommGrpCat.Colimits.quotToQuotUlift · cited by 1Colimits.quotToQuotUliftAddCommGrpCat.Colimits.quotToQuotUlift_ι · cited by 1Colimits.quotToQuotUlift_ιAddCommGrpCat.Colimits.quotUliftToQuot · cited by 1Colimits.quotUliftToQuotAddCommGrpCat.Colimits.quotUliftToQuot_ι · cited by 0Colimits.quotUliftToQuot_ιAddCommGrpCat.uliftZMultiplesAddEquiv_symm_apply_hom_apply · cited by 0AddCommGrpCat.uliftZMulti…Equiv · cited by 8337EquivAddEquiv · cited by 1087AddEquivEquiv.ulift · cited by 115Equiv.uliftAddEquiv.uliftCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by28

Results whose statement or proof uses this declaration.