Rat

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

Statistics

Metric	Count
Definitions	0
Theorems toPosSMulStrictMono_rat, toPosSMulStrictMono_rat, nnrat_of_rat, nnrat_of_rat, abs_nnqsmul	5
Total	5

LinearOrderedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPosSMulStrictMono_rat 📖	mathematical	—	PosSMulStrictMono Rat.smulDivisionRing Field.toDivisionRing Rat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing	—	Rat.smul_def mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono Rat.cast_pos

LinearOrderedSemifield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPosSMulStrictMono_rat 📖	mathematical	—	PosSMulStrictMono NNRat NNRat.smulDivisionSemiring Semifield.toDivisionSemiring PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring NNRat.instSemifield	—	NNRat.smul_def mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono NNRat.cast_pos

PosSMulMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnrat_of_rat 📖	mathematical	—	PosSMulMono NNRat SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield MulAction.toSemigroupAction PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	NNRat.cast_smul_eq_nnqsmul smul_le_smul_of_nonneg_left

PosSMulStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnrat_of_rat 📖	mathematical	—	PosSMulStrictMono NNRat SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield MulAction.toSemigroupAction PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	NNRat.cast_smul_eq_nnqsmul smul_lt_smul_of_pos_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_nnqsmul 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	le_total abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono smul_neg abs_of_nonneg

---

← Back to Index