ULift

Statistics

Metric	Count
Definitions `addAction`, `addAction'`, `distribMulAction`, `distribMulAction'`, `distribSMul`, `distribSMul'`, `module'`, `moduleEquiv`, `mulAction`, `mulAction'`, `mulActionWithZero`, `mulActionWithZero'`, `mulDistribMulAction`, `mulDistribMulAction'`, `smulLeft`, `smulWithZero`, `smulWithZero'`, `smulZeroClass`, `smulZeroClass'`, `vaddLeft`	20
Theorems `instIsCentralScalar`, `isScalarTower`, `isScalarTower'`, `isScalarTower''`, `moduleEquiv_apply`, `moduleEquiv_symm_apply`, `smul_def`, `vadd_def`	8
Total	28

Name	Category	Theorems
`addAction` 📖	CompOp	—
`addAction'` 📖	CompOp	—
`distribMulAction` 📖	CompOp	—
`distribMulAction'` 📖	CompOp	—
`distribSMul` 📖	CompOp	—
`distribSMul'` 📖	CompOp	—
`module'` 📖	CompOp	13 math math: `Module.ulift_injective_of_injective`, `moduleEquiv_symm_apply`, `instModuleIsReflexive`, `Module.Finite.ulift`, `rank_ulift`, `Module.injective_iff_ulift_injective`, `ModuleCat.uliftFunctor_map`, `ModuleCat.uliftFunctor_obj`, `finrank_ulift`, `Module.Flat.ulift`, `Module.Free.ulift`, `moduleEquiv_apply`, `ModuleCat.ulift_injective_of_injective`
`moduleEquiv` 📖	CompOp	3 math math: `moduleEquiv_symm_apply`, `ModuleCat.uliftFunctor_map`, `moduleEquiv_apply`
`mulAction` 📖	CompOp	—
`mulAction'` 📖	CompOp	—
`mulActionWithZero` 📖	CompOp	—
`mulActionWithZero'` 📖	CompOp	—
`mulDistribMulAction` 📖	CompOp	—
`mulDistribMulAction'` 📖	CompOp	—
`smulLeft` 📖	CompOp	6 math math: `isScalarTower`, `isIsometricSMul`, `instContinuousSMulULift`, `smul_def`, `instContinuousConstSMulULift`, `isScalarTower'`
`smulWithZero` 📖	CompOp	—
`smulWithZero'` 📖	CompOp	—
`smulZeroClass` 📖	CompOp	—
`smulZeroClass'` 📖	CompOp	—
`vaddLeft` 📖	CompOp	4 math math: `instContinuousConstVAddULift`, `instContinuousVAddULift`, `isIsometricVAdd`, `vadd_def`

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `smul` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `smulLeft`	—	`smul_assoc`
`isScalarTower'` 📖	mathematical	—	`IsScalarTower` `smul` `smulLeft`	—	`smul_assoc`
`isScalarTower''` 📖	mathematical	—	`IsScalarTower` `smul`	—	`smul_assoc`
`moduleEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `addCommMonoid` `module'` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `moduleEquiv`	—	`RingHomInvPair.ids`
`moduleEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `addCommMonoid` `module'` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `moduleEquiv`	—	`RingHomInvPair.ids`
`smul_def` 📖	mathematical	—	`smulLeft`	—	—
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `vaddLeft`	—	—

---