PartialSups

📁 Source: Mathlib/Algebra/Order/Group/PartialSups.lean

Statistics

Metric	Count
Definitions	0
Theorems partialSups_add_const, partialSups_const_add, partialSups_const_mul, partialSups_mul_const	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups_add_const 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	map_partialSups OrderIsoClass.toSupHomClass OrderIso.instOrderIsoClass
partialSups_const_add 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	map_partialSups OrderIsoClass.toSupHomClass OrderIso.instOrderIsoClass
partialSups_const_mul 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	map_partialSups OrderIsoClass.toSupHomClass OrderIso.instOrderIsoClass
partialSups_mul_const 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	map_partialSups OrderIsoClass.toSupHomClass OrderIso.instOrderIsoClass

---

← Back to Index