Mathlib Map

Theorems · Definition

MulEquiv.ulift

{α : Type u} → [inst : Mul α] → ULift.{u_1, u} α ≃* α

The multiplicative equivalence between ULift α and α.

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

Around this declaration

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

MonCat.uliftFunctor · cited by 2MonCat.uliftFunctorCommMonCat.uliftFunctor · cited by 2CommMonCat.uliftFunctoruliftPowersHom · cited by 2uliftPowersHomCommGrpCat.uliftFunctor · cited by 2CommGrpCat.uliftFunctoruliftZPowersHom · cited by 2uliftZPowersHomGrpCat.uliftFunctor · cited by 2GrpCat.uliftFunctorCommMonCat.uliftFunctor_map · cited by 0CommMonCat.uliftFunctor_m…uliftPowersHom_apply_apply · cited by 0uliftPowersHom_apply_applyuliftPowersHom_symm_apply · cited by 0uliftPowersHom_symm_applyCommGrpCat.uliftFunctor_map · cited by 0CommGrpCat.uliftFunctor_m…MonCat.uliftFunctor_map · cited by 0MonCat.uliftFunctor_mapCommGrpCat.uliftFunctorFullyFaithful · cited by 0CommGrpCat.uliftFunctorFu…uliftZPowersHom_apply_apply · cited by 0uliftZPowersHom_apply_app…uliftZPowersHom_symm_apply · cited by 0uliftZPowersHom_symm_applyGrpCat.uliftFunctorFullyFaithful · cited by 0GrpCat.uliftFunctorFullyF…Equiv · cited by 8337EquivMulEquiv · cited by 1142MulEquivEquiv.ulift · cited by 115Equiv.uliftMulEquiv.uliftCITED BYCITES

Cites3

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

Cited by16

Results whose statement or proof uses this declaration.