Lemmas

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

Statistics

Metric	Count
Definitions `WithStrictness`, `addRelRelData`, `divRelConstData`, `mulConstRelData`, `mulRelConstData`, `rearrangeData`, `relImpRelData`, `smulConstRelData`, `smulRelConstData`	9
Theorems `add_eq_eq`, `add_eq_le`, `add_eq_lt`, `add_le_eq`, `add_lt_eq`, `div_eq_const`, `div_le_const`, `div_lt_const`, `div_lt_const_weak`, `eq_of_add_pow`, `eq_of_eq`, `eq_rearrange`, `le_of_eq`, `le_of_le`, `le_of_lt`, `le_rearrange`, `lt_of_eq`, `lt_of_le`, `lt_of_lt`, `lt_rearrange`, `mul_const_eq`, `mul_const_le`, `mul_const_lt`, `mul_const_lt_weak`, `mul_eq_const`, `mul_le_const`, `mul_lt_const`, `mul_lt_const_weak`, `smul_const_eq`, `smul_const_le`, `smul_const_lt`, `smul_const_lt_weak`, `smul_eq_const`, `smul_le_const`, `smul_lt_const`, `smul_lt_const_weak`	36
Total	45

Mathlib.Ineq

Definitions

Name	Category	Theorems
`WithStrictness` 📖	CompData	—
`addRelRelData` 📖	CompOp	—
`divRelConstData` 📖	CompOp	—
`mulConstRelData` 📖	CompOp	—
`mulRelConstData` 📖	CompOp	—
`rearrangeData` 📖	CompOp	—
`relImpRelData` 📖	CompOp	—
`smulConstRelData` 📖	CompOp	—
`smulRelConstData` 📖	CompOp	—

Mathlib.Tactic.LinearCombination

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_eq` 📖	—	—	—	—	—
`add_eq_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono`
`add_eq_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_lt_add_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid`
`add_le_eq` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`add_lt_eq` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid`
`div_eq_const` 📖	—	—	—	—	—
`div_le_const` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono`
`div_lt_const` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_lt_div_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono`
`div_lt_const_weak` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `LT.lt.le`
`eq_of_add_pow` 📖	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—	`sub_eq_zero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors`
`eq_of_eq` 📖	—	—	—	—	`add_right_cancel`
`eq_rearrange` 📖	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`sub_eq_zero`
`le_of_eq` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`le_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right`
`le_of_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`le_of_le` `LT.lt.le`
`le_rearrange` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`sub_nonpos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`lt_of_eq` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`lt_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `lt_imp_lt_of_le_of_le` `le_refl` `add_le_add_right`
`lt_of_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `lt_imp_lt_of_le_of_le` `le_refl` `add_lt_add_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd`
`lt_rearrange` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`sub_neg` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`mul_const_eq` 📖	—	—	—	—	—
`mul_const_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono`
`mul_const_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_lt_mul_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono`
`mul_const_lt_weak` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `LT.lt.le`
`mul_eq_const` 📖	—	—	—	—	—
`mul_le_const` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono`
`mul_lt_const` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono`
`mul_lt_const_weak` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `LT.lt.le`
`smul_const_eq` 📖	—	—	—	—	—
`smul_const_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`smul_le_smul_of_nonneg_left`
`smul_const_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`smul_lt_smul_of_pos_left`
`smul_const_lt_weak` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`smul_le_smul_of_nonneg_left` `LT.lt.le`
`smul_eq_const` 📖	—	—	—	—	—
`smul_le_const` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_le_smul_of_nonneg_right` `PosSMulMono.toSMulPosMono` `IsOrderedModule.toPosSMulMono`
`smul_lt_const` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_lt_smul_of_pos_right` `PosSMulStrictMono.toSMulPosStrictMono` `IsStrictOrderedModule.toPosSMulStrictMono`
`smul_lt_const_weak` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_le_smul_of_nonneg_right` `PosSMulMono.toSMulPosMono` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `LT.lt.le`

---

← Back to Index