Field

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

Statistics

Metric	Count
Definitions evalSMul, smulRightDual	2
Theorems smul_ne_zero_of_ne_zero_of_pos, smul_ne_zero_of_pos_of_ne_zero, smul_nonneg_of_nonneg_of_pos, smul_nonneg_of_pos_of_nonneg, smul_nonneg_of_pos_of_pos, smulRightDual_apply, smulRightDual_symm_apply, toPosSMulReflectLE, toPosSMulReflectLT, inv_smul_le_iff_of_neg, inv_smul_lt_iff_of_neg, smul_inv_le_iff_of_neg, smul_inv_lt_iff_of_neg	13
Total	15

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalSMul 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_ne_zero_of_ne_zero_of_pos 📖	—	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	smul_ne_zero IsDomain.toIsCancelMulZero LT.lt.ne'
smul_ne_zero_of_pos_of_ne_zero 📖	—	Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	smul_ne_zero IsDomain.toIsCancelMulZero LT.lt.ne'
smul_nonneg_of_nonneg_of_pos 📖	mathematical	Preorder.toLE Preorder.toLT	SMulZeroClass.toSMul	—	smul_nonneg LT.lt.le
smul_nonneg_of_pos_of_nonneg 📖	mathematical	Preorder.toLT Preorder.toLE	SMulZeroClass.toSMul	—	smul_nonneg LT.lt.le
smul_nonneg_of_pos_of_pos 📖	mathematical	Preorder.toLT	Preorder.toLE SMulZeroClass.toSMul	—	smul_nonneg LT.lt.le

OrderIso

Definitions

Name	Category	Theorems
smulRightDual 📖	CompOp	2 math math: smulRightDual_apply, smulRightDual_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smulRightDual_apply 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	DFunLike.coe RelIso OrderDual Preorder.toLE OrderDual.instLE RelIso.instFunLike smulRightDual OrderDual.instSMul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield MulAction.toSemigroupAction DistribMulAction.toMulAction Semiring.toMonoidWithZero Ring.toSemiring DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction AddCommGroup.toAddCommMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—
smulRightDual_symm_apply 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	DFunLike.coe RelIso OrderDual OrderDual.instLE Preorder.toLE RelIso.instFunLike RelIso.symm smulRightDual SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield MulAction.toSemigroupAction DistribMulAction.toMulAction Semiring.toMonoidWithZero Ring.toSemiring DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	—

PosSMulMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPosSMulReflectLE 📖	mathematical	—	PosSMulReflectLE SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulAction.toSemigroupAction PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	inv_smul_smul₀ LT.lt.ne' smul_le_smul_of_nonneg_left inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono LT.lt.le

PosSMulStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPosSMulReflectLT 📖	mathematical	—	PosSMulReflectLT SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulActionWithZero.toSMulWithZero PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	PosSMulReflectLT.of_pos inv_smul_smul₀ LT.lt.ne' smul_lt_smul_of_pos_left inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_smul_le_iff_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Preorder.toLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	smul_le_smul_iff_of_neg_left IsStrictOrderedRing.toIsOrderedRing PosSMulReflectLT.toPosSMulReflectLE IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors PosSMulReflectLE.toPosSMulReflectLT PosSMulMono.toPosSMulReflectLE smul_inv_smul₀ LT.lt.ne
inv_smul_lt_iff_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	smul_lt_smul_iff_of_neg_left IsStrictOrderedRing.toIsOrderedRing PosSMulStrictMono.toPosSMulReflectLT smul_inv_smul₀ LT.lt.ne
smul_inv_le_iff_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Preorder.toLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	smul_le_smul_iff_of_neg_left IsStrictOrderedRing.toIsOrderedRing PosSMulReflectLT.toPosSMulReflectLE IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors PosSMulReflectLE.toPosSMulReflectLT PosSMulMono.toPosSMulReflectLE smul_inv_smul₀ LT.lt.ne
smul_inv_lt_iff_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	smul_lt_smul_iff_of_neg_left IsStrictOrderedRing.toIsOrderedRing PosSMulStrictMono.toPosSMulReflectLT smul_inv_smul₀ LT.lt.ne

---

← Back to Index