Lemmas

📁 Source: Mathlib/Tactic/Linarith/Lemmas.lean

Statistics

Metric	Count
Definitions toConstMulName	1
Theorems add_lt_of_le_of_neg, add_lt_of_neg_of_le, add_neg, add_nonpos, eq_of_eq_of_eq, eq_of_not_lt_of_not_gt, le_of_eq_of_le, le_of_le_of_eq, lt_irrefl, lt_of_eq_of_lt, lt_of_lt_of_eq, mul_eq, mul_neg, mul_nonpos, mul_zero_eq, natCast_nonneg, sub_neg_of_lt, sub_nonpos_of_le, zero_lt_one, zero_mul_eq	20
Total	21

Mathlib.Ineq

Definitions

Name	Category	Theorems
toConstMulName 📖	CompOp	—

Mathlib.Tactic.Linarith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_lt_of_le_of_neg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	add_lt_of_le_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
add_lt_of_neg_of_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	add_lt_of_neg_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
add_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	add_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
add_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	add_nonpos IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
eq_of_eq_of_eq 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	add_zero
eq_of_not_lt_of_not_gt 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	le_antisymm le_of_not_gt
le_of_eq_of_le 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	zero_add
le_of_le_of_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	add_zero
lt_irrefl 📖	mathematical	—	Preorder.toLT	—	lt_irrefl
lt_of_eq_of_lt 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLT PartialOrder.toPreorder	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	zero_add
lt_of_lt_of_eq 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	add_zero
mul_eq 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLT PartialOrder.toPreorder	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.mul_zero
mul_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsStrictOrderedRing.toIsOrderedCancelAddMonoid neg_neg_of_pos neg_of_neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd neg_mul
mul_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Preorder.toLT	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid le_of_lt neg_neg_of_pos neg_mul
mul_zero_eq 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.mul_zero
natCast_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Nat.cast_nonneg
sub_neg_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sub_neg_of_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
sub_nonpos_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sub_nonpos_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
zero_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
zero_mul_eq 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.zero_mul

---

← Back to Index