ULift

📁 Source: Mathlib/Algebra/Group/ULift.lean

Statistics

Metric	Count
Definitions `ulift`, `ulift`, `add`, `addCancelCommMonoid`, `addCancelMonoid`, `addCommGroup`, `addCommMonoid`, `addCommSemigroup`, `addGroup`, `addLeftCancelMonoid`, `addLeftCancelSemigroup`, `addMonoid`, `addRightCancelMonoid`, `addRightCancelSemigroup`, `addSemigroup`, `addZeroClass`, `cancelCommMonoid`, `cancelMonoid`, `commGroup`, `commMonoid`, `commSemigroup`, `div`, `divInvMonoid`, `group`, `inv`, `leftCancelMonoid`, `leftCancelSemigroup`, `monoid`, `mul`, `mulOneClass`, `neg`, `one`, `pow`, `rightCancelMonoid`, `rightCancelSemigroup`, `semigroup`, `smul`, `sub`, `subNegAddMonoid`, `vadd`, `zero`	41
Theorems `add_down`, `div_down`, `inv_down`, `mul_down`, `neg_down`, `nontrivial`, `one_down`, `pow_down`, `smul_down`, `sub_down`, `vadd_down`, `zero_down`	12
Total	53

AddEquiv

Definitions

Name	Category	Theorems
`ulift` 📖	CompOp	11 math math: `AddMonCat.uliftFunctor_map`, `uliftMultiplesHom_symm_apply`, `AddGrpCat.uliftFunctor_map`, `CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply`, `uliftMultiplesHom_apply_apply`, `CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply`, `uliftZMultiplesHom_apply_apply`, `AddCommGrpCat.uliftFunctor_map`, `AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv`, `AddCommMonCat.uliftFunctor_map`, `uliftZMultiplesHom_symm_apply`

MulEquiv

Definitions

Name	Category	Theorems
`ulift` 📖	CompOp	8 math math: `CommGrpCat.uliftFunctor_map`, `uliftZPowersHom_symm_apply`, `uliftPowersHom_symm_apply`, `uliftPowersHom_apply_apply`, `MonCat.uliftFunctor_map`, `CommMonCat.uliftFunctor_map`, `uliftZPowersHom_apply_apply`, `GrpCat.uliftFunctor_map`

ULift

Definitions

Name	Category	Theorems
`add` 📖	CompOp	15 math math: `AddMonCat.uliftFunctor_map`, `isAddLeftRegular_up`, `AddGrpCat.uliftFunctor_map`, `CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply`, `instContinuousAddULift`, `isAddRightRegular_up`, `CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply`, `AddCommGrpCat.uliftFunctor_map`, `isAddRightRegular_down`, `isAddRegular_down`, `AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv`, `add_down`, `isAddLeftRegular_down`, `isAddRegular_up`, `AddCommMonCat.uliftFunctor_map`
`addCancelCommMonoid` 📖	CompOp	—
`addCancelMonoid` 📖	CompOp	—
`addCommGroup` 📖	CompOp	7 math math: `Module.ulift_injective_of_injective`, `AddCommGrpCat.uliftFunctor_map`, `AddCommGrpCat.uliftFunctor_obj`, `Module.injective_iff_ulift_injective`, `ModuleCat.uliftFunctor_map`, `ModuleCat.uliftFunctor_obj`, `ModuleCat.ulift_injective_of_injective`
`addCommMonoid` 📖	CompOp	10 math math: `moduleEquiv_symm_apply`, `instModuleIsReflexive`, `Module.Finite.ulift`, `rank_ulift`, `ModuleCat.uliftFunctor_map`, `finrank_ulift`, `Module.Flat.ulift`, `Module.Free.ulift`, `moduleEquiv_apply`, `AddCommMonCat.uliftFunctor_map`
`addCommSemigroup` 📖	CompOp	—
`addGroup` 📖	CompOp	2 math math: `AddGrpCat.uliftFunctor_obj`, `AddGrpCat.uliftFunctor_map`
`addLeftCancelMonoid` 📖	CompOp	—
`addLeftCancelSemigroup` 📖	CompOp	—
`addMonoid` 📖	CompOp	1 math math: `AddMonCat.uliftFunctor_map`
`addRightCancelMonoid` 📖	CompOp	—
`addRightCancelSemigroup` 📖	CompOp	—
`addSemigroup` 📖	CompOp	—
`addZeroClass` 📖	CompOp	9 math math: `AddMonCat.uliftFunctor_map`, `uliftMultiplesHom_symm_apply`, `AddGrpCat.uliftFunctor_map`, `uliftMultiplesHom_apply_apply`, `uliftZMultiplesHom_apply_apply`, `AddCommGrpCat.uliftFunctor_map`, `AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv`, `AddCommMonCat.uliftFunctor_map`, `uliftZMultiplesHom_symm_apply`
`cancelCommMonoid` 📖	CompOp	—
`cancelMonoid` 📖	CompOp	—
`commGroup` 📖	CompOp	2 math math: `CommGrpCat.uliftFunctor_map`, `CommGrpCat.uliftFunctor_obj`
`commMonoid` 📖	CompOp	1 math math: `CommMonCat.uliftFunctor_map`
`commSemigroup` 📖	CompOp	—
`div` 📖	CompOp	1 math math: `div_down`
`divInvMonoid` 📖	CompOp	—
`group` 📖	CompOp	3 math math: `instIsTopologicalGroupULift`, `GrpCat.uliftFunctor_map`, `GrpCat.uliftFunctor_obj`
`inv` 📖	CompOp	2 math math: `instContinuousInvULift`, `inv_down`
`leftCancelMonoid` 📖	CompOp	—
`leftCancelSemigroup` 📖	CompOp	—
`monoid` 📖	CompOp	1 math math: `MonCat.uliftFunctor_map`
`mul` 📖	CompOp	12 math math: `CommGrpCat.uliftFunctor_map`, `isLeftRegular_up`, `isRightRegular_up`, `isLeftRegular_down`, `mul_down`, `MonCat.uliftFunctor_map`, `isRightRegular_down`, `isRegular_down`, `CommMonCat.uliftFunctor_map`, `isRegular_up`, `GrpCat.uliftFunctor_map`, `instContinuousMulULift`
`mulOneClass` 📖	CompOp	8 math math: `CommGrpCat.uliftFunctor_map`, `uliftZPowersHom_symm_apply`, `uliftPowersHom_symm_apply`, `uliftPowersHom_apply_apply`, `MonCat.uliftFunctor_map`, `CommMonCat.uliftFunctor_map`, `uliftZPowersHom_apply_apply`, `GrpCat.uliftFunctor_map`
`neg` 📖	CompOp	2 math math: `instContinuousNegULift`, `neg_down`
`one` 📖	CompOp	2 math math: `one_down`, `normOneClass`
`pow` 📖	CompOp	1 math math: `pow_down`
`rightCancelMonoid` 📖	CompOp	—
`rightCancelSemigroup` 📖	CompOp	—
`semigroup` 📖	CompOp	—
`smul` 📖	CompOp	7 math math: `isIsometricSMul'`, `smul_down`, `isScalarTower''`, `isSMulRegular_iff`, `isScalarTower'`, `instIsCentralScalar`, `instNormSMulClass`
`sub` 📖	CompOp	1 math math: `sub_down`
`subNegAddMonoid` 📖	CompOp	—
`vadd` 📖	CompOp	2 math math: `isIsometricVAdd'`, `vadd_down`
`zero` 📖	CompOp	1 math math: `zero_down`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_down` 📖	mathematical	—	`add`	—	—
`div_down` 📖	mathematical	—	`div`	—	—
`inv_down` 📖	mathematical	—	`inv`	—	—
`mul_down` 📖	mathematical	—	`mul`	—	—
`neg_down` 📖	mathematical	—	`neg`	—	—
`nontrivial` 📖	mathematical	—	`Nontrivial`	—	`Function.Injective.nontrivial` `Equiv.injective`
`one_down` 📖	mathematical	—	`one`	—	—
`pow_down` 📖	mathematical	—	`pow`	—	—
`smul_down` 📖	mathematical	—	`smul`	—	—
`sub_down` 📖	mathematical	—	`sub`	—	—
`vadd_down` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `vadd`	—	—
`zero_down` 📖	mathematical	—	`zero`	—	—

---

← Back to Index