Ineq

📁 Source: Mathlib/Tactic/NormNum/Ineq.lean

Statistics

Metric	Count
Definitions Ineq, evalLE, evalLT, inferLinearOrderedField, inferLinearOrderedSemifield, inferOrderedRing, inferOrderedSemiring	7
Theorems isInt_le_false, isInt_le_true, isInt_lt_false, isInt_lt_true, isNNRat_le_false, isNNRat_le_true, isNNRat_lt_false, isNNRat_lt_true, isNat_le_false, isNat_le_true, isNat_lt_false, isNat_lt_true, isRat_le_false, isRat_le_true, isRat_lt_false, isRat_lt_true	16
Total	23

Mathlib

Definitions

Name	Category	Theorems
Ineq 📖	CompData	—

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalLE 📖	CompOp	—
evalLT 📖	CompOp	—
inferLinearOrderedField 📖	CompOp	—
inferLinearOrderedSemifield 📖	CompOp	—
inferOrderedRing 📖	CompOp	—
inferOrderedSemiring 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInt_le_false 📖	mathematical	IsInt	Preorder.toLE PartialOrder.toPreorder	—	not_le_of_gt isInt_lt_true
isInt_le_true 📖	mathematical	IsInt	Preorder.toLE PartialOrder.toPreorder	—	Int.cast_mono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
isInt_lt_false 📖	mathematical	IsInt	Preorder.toLT PartialOrder.toPreorder	—	not_lt_of_ge isInt_le_true
isInt_lt_true 📖	mathematical	IsInt	Preorder.toLT PartialOrder.toPreorder	—	Int.cast_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass NeZero.one
isNNRat_le_false 📖	mathematical	IsNNRat	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	not_le_of_gt isNNRat_lt_true
isNNRat_le_true 📖	mathematical	IsNNRat	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero invOf_nonneg Nat.cast_nonneg mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Nat.commute_cast Nat.cast_mul mul_invOf_cancel_right' mul_assoc
isNNRat_lt_false 📖	mathematical	IsNNRat	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	not_lt_of_ge isNNRat_le_true
isNNRat_lt_true 📖	mathematical	IsNNRat	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero pos_invOf_of_invertible_cast mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Nat.commute_cast Nat.cast_mul mul_invOf_cancel_right' mul_assoc
isNat_le_false 📖	mathematical	IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Preorder.toLE PartialOrder.toPreorder	—	not_le_of_gt isNat_lt_true
isNat_le_true 📖	mathematical	IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Preorder.toLE PartialOrder.toPreorder	—	Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
isNat_lt_false 📖	mathematical	IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Preorder.toLT PartialOrder.toPreorder	—	not_lt_of_ge isNat_le_true
isNat_lt_true 📖	mathematical	IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Preorder.toLT PartialOrder.toPreorder	—	Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ble_eq_false
isRat_le_false 📖	mathematical	IsRat	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	not_le_of_gt isRat_lt_true
isRat_le_true 📖	mathematical	IsRat	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Int.cast_mono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass invOf_nonneg Nat.cast_nonneg mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Int.commute_cast Int.cast_mul Int.cast_natCast mul_invOf_cancel_right' mul_assoc
isRat_lt_false 📖	mathematical	IsRat	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	not_lt_of_ge isRat_le_true
isRat_lt_true 📖	mathematical	IsRat	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Int.cast_strictMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero pos_invOf_of_invertible_cast mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Int.commute_cast Int.cast_mul Int.cast_natCast mul_invOf_cancel_right' mul_assoc

---

← Back to Index