OrderedSMul

📁 Source: Mathlib/Algebra/Order/Module/OrderedSMul.lean

Statistics

Metric	Count
Definitions OrderedSMul	1
Theorems orderedSMul, toOrderedSMul, orderedSMul, instOrderedSMul, lt_of_smul_lt_smul_of_pos, mk', mk'', smul_lt_smul_of_pos, toPosSMulReflectLT, toPosSMulStrictMono, orderedSMul, instOrderedSMulProd	12
Total	13

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderedSMul 📖	mathematical	—	OrderedSMul instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AddCommGroup.toAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder instSMulWithZeroInt SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	OrderedSMul.mk'' natCast_zsmul strictMono_smul_left_of_pos instPosSMulStrictMonoNatOfIsOrderedAddMonoid

LinearOrderedSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toOrderedSMul 📖	mathematical	—	OrderedSMul SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toSMulWithZero NonUnitalNonAssocSemiring.toMulZeroClass	—	OrderedSMul.mk'' strictMono_mul_left_of_pos IsStrictOrderedRing.toPosMulStrictMono

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderedSMul 📖	mathematical	—	OrderedSMul instSemiring instPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instSMulWithZeroNat AddCommMonoid.toAddMonoid	—	OrderedSMul.mk'' one_nsmul succ_nsmul add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd covariant_swap_add_of_covariant_add

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instOrderedSMul 📖	mathematical	—	OrderedSMul OrderDual instAddCommMonoid instPartialOrder instSMulWithZero' MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	OrderedSMul.smul_lt_smul_of_pos OrderedSMul.lt_of_smul_lt_smul_of_pos

OrderedSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lt_of_smul_lt_smul_of_pos 📖	—	Preorder.toLT PartialOrder.toPreorder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	—
mk' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulActionWithZero.toSMulWithZero	OrderedSMul	—	LE.le.lt_of_ne IsUnit.smul_left_cancel Ne.isUnit LT.lt.ne' LT.lt.ne inv_smul_smul pos_of_mul_pos_right Units.mul_inv IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero LT.lt.le
mk'' 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	OrderedSMul	—	StrictMono.lt_iff_lt
smul_lt_smul_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass	—	—
toPosSMulReflectLT 📖	mathematical	—	PosSMulReflectLT SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PartialOrder.toPreorder	—	PosSMulReflectLT.of_pos lt_of_smul_lt_smul_of_pos
toPosSMulStrictMono 📖	mathematical	—	PosSMulStrictMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PartialOrder.toPreorder	—	smul_lt_smul_of_pos

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderedSMul 📖	mathematical	OrderedSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	addCommMonoid partialOrder smulWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	OrderedSMul.mk' smul_le_smul_of_nonneg_left PosSMulStrictMono.toPosSMulMono OrderedSMul.toPosSMulStrictMono LT.lt.le

(root)

Definitions

Name	Category	Theorems
OrderedSMul 📖	CompData	7 math math: OrderDual.instOrderedSMul, instOrderedSMulProd, Int.orderedSMul, LinearOrderedSemiring.toOrderedSMul, Nat.orderedSMul, OrderedSMul.mk'', OrderedSMul.mk'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instOrderedSMulProd 📖	mathematical	—	OrderedSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Prod.instAddCommMonoid Prod.instPartialOrder Prod.smulWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero	—	OrderedSMul.mk' smul_le_smul_of_nonneg_left PosSMulStrictMono.toPosSMulMono OrderedSMul.toPosSMulStrictMono LT.lt.le

---

← Back to Index