Defs

📁 Source: Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean

Statistics

Metric	Count
Definitions `AddLeftMono`, `AddLeftReflectLE`, `AddLeftReflectLT`, `AddLeftStrictMono`, `AddRightMono`, `AddRightReflectLE`, `AddRightReflectLT`, `AddRightStrictMono`, `Contravariant`, `ContravariantClass`, `Covariant`, `CovariantClass`, `MulLeftMono`, `MulLeftReflectLE`, `MulLeftReflectLT`, `MulLeftStrictMono`, `MulRightMono`, `MulRightReflectLE`, `MulRightReflectLT`, `MulRightStrictMono`	20
Theorems `addLeftReflectLE_of_addLeftMono`, `addLeftReflectLT_of_addLeftStrictMono`, `addRightReflectLE_of_addRightMono`, `addRightReflectLT_of_addRightStrictMono`, `covariant_iff_contravariant`, `covariant_swap_iff_contravariant_swap`, `covconv`, `covconv_swap`, `covariant_of_const`, `covariant_of_const'`, `flip`, `elim`, `flip`, `monotone_of_const`, `elim`, `covariant_iff_contravariant`, `covariant_swap_iff_contravariant_swap`, `covconv`, `covconv_swap`, `mulLeftReflectLE_of_mulLeftMono`, `mulLeftReflectLT_of_mulLeftStrictMono`, `mulRightReflectLE_of_mulRightMono`, `mulRightReflectLT_of_mulRightStrictMono`, `addLeftReflectLE_of_addLeftReflectLT`, `addLeftStrictMono_of_addLeftMono`, `mulLeftReflectLE_of_mulLeftReflectLT`, `mulLeftStrictMono_of_mulLeftMono`, `addRightReflectLE_of_addRightReflectLT`, `addRightStrictMono_of_addRightMono`, `mulRightReflectLE_of_mulRightReflectLT`, `mulRightStrictMono_of_mulRightMono`, `covariant_of_const`, `covariant_of_const'`, `act_rel_act_of_rel`, `act_rel_act_of_rel_of_rel`, `act_rel_of_act_rel_of_rel_act_rel`, `act_rel_of_rel_of_act_rel`, `addLeftMono_of_addLeftStrictMono`, `addLeftReflectLT_of_addLeftMono`, `addLeftStrictMono_of_addLeftReflectLE`, `addRightMono_of_addLeftMono`, `addRightMono_of_addRightStrictMono`, `addRightReflectLE_of_addLeftReflectLE`, `addRightReflectLT_of_addLeftReflectLT`, `addRightReflectLT_of_addRightMono`, `addRightStrictMono_of_addLeftStrictMono`, `addRightStrictMono_of_addRightReflectLE`, `contravariant_flip_iff`, `contravariant_le_iff_contravariant_lt_and_eq`, `contravariant_le_of_contravariant_eq_and_lt`, `contravariant_lt_of_contravariant_le`, `contravariant_lt_of_covariant_le`, `contravariant_swap_add_of_contravariant_add`, `contravariant_swap_mul_of_contravariant_mul`, `covariantClass_le_of_lt`, `covariant_flip_iff`, `covariant_le_iff_contravariant_lt`, `covariant_le_of_covariant_lt`, `covariant_lt_iff_contravariant_le`, `covariant_lt_of_contravariant_le`, `covariant_lt_of_covariant_le_of_contravariant_eq`, `covariant_swap_add_of_covariant_add`, `covariant_swap_mul_of_covariant_mul`, `instOrderedAddOfAddRightMonoOfAddRightReflectLE`, `mulLeftMono_of_mulLeftStrictMono`, `mulLeftReflectLT_of_mulLeftMono`, `mulLeftStrictMono_of_mulLeftReflectLE`, `mulRightMono_of_mulLeftMono`, `mulRightMono_of_mulRightStrictMono`, `mulRightReflectLE_of_mulLeftReflectLE`, `mulRightReflectLT_of_mulLeftReflectLT`, `mulRightReflectLT_of_mulRightMono`, `mulRightStrictMono_of_mulLeftStrictMono`, `mulRightStrictMono_of_mulRightReflectLE`, `rel_act_of_act_rel_act_of_rel_act`, `rel_act_of_rel_of_rel_act`, `rel_iff_cov`, `rel_of_act_rel_act`	78
Total	98

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftReflectLE_of_addLeftMono` 📖	mathematical	—	`AddLeftReflectLE` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`covconv`
`addLeftReflectLT_of_addLeftStrictMono` 📖	mathematical	—	`AddLeftReflectLT` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`covconv`
`addRightReflectLE_of_addRightMono` 📖	mathematical	—	`AddRightReflectLE` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`covconv_swap`
`addRightReflectLT_of_addRightStrictMono` 📖	mathematical	—	`AddRightReflectLT` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`covconv_swap`
`covariant_iff_contravariant` 📖	mathematical	—	`Covariant` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `Contravariant`	—	`neg_add_cancel_left`
`covariant_swap_iff_contravariant_swap` 📖	mathematical	—	`Covariant` `Function.swap` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `Contravariant`	—	`add_neg_cancel_right`
`covconv` 📖	mathematical	—	`ContravariantClass` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`covariant_iff_contravariant` `CovariantClass.elim`
`covconv_swap` 📖	mathematical	—	`ContravariantClass` `Function.swap` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`covariant_swap_iff_contravariant_swap` `CovariantClass.elim`

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covariant_of_const` 📖	—	`Antitone`	—	—	`comp_monotone` `Covariant.monotone_of_const`
`covariant_of_const'` 📖	—	`Antitone`	—	—	`covariant_of_const`

Contravariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip` 📖	—	`Contravariant`	—	—	—

ContravariantClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim` 📖	mathematical	—	`Contravariant`	—	—

Covariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip` 📖	—	`Covariant`	—	—	—
`monotone_of_const` 📖	mathematical	—	`Monotone`	—	`CovariantClass.elim`

CovariantClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim` 📖	mathematical	—	`Covariant`	—	—

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covariant_iff_contravariant` 📖	mathematical	—	`Covariant` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid` `Contravariant`	—	`inv_mul_cancel_left`
`covariant_swap_iff_contravariant_swap` 📖	mathematical	—	`Covariant` `Function.swap` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid` `Contravariant`	—	`mul_inv_cancel_right`
`covconv` 📖	mathematical	—	`ContravariantClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`covariant_iff_contravariant` `CovariantClass.elim`
`covconv_swap` 📖	mathematical	—	`ContravariantClass` `Function.swap` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`covariant_swap_iff_contravariant_swap` `CovariantClass.elim`
`mulLeftReflectLE_of_mulLeftMono` 📖	mathematical	—	`MulLeftReflectLE` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`covconv`
`mulLeftReflectLT_of_mulLeftStrictMono` 📖	mathematical	—	`MulLeftReflectLT` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`covconv`
`mulRightReflectLE_of_mulRightMono` 📖	mathematical	—	`MulRightReflectLE` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`covconv_swap`
`mulRightReflectLT_of_mulRightStrictMono` 📖	mathematical	—	`MulRightReflectLT` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`covconv_swap`

IsLeftCancelAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftReflectLE_of_addLeftReflectLT` 📖	mathematical	—	`AddLeftReflectLE` `Preorder.toLE` `PartialOrder.toPreorder`	—	`contravariant_le_iff_contravariant_lt_and_eq` `ContravariantClass.elim` `add_left_cancel`
`addLeftStrictMono_of_addLeftMono` 📖	mathematical	—	`AddLeftStrictMono` `Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.lt_of_ne` `CovariantClass.elim` `LT.lt.le` `add_ne_add_right` `LT.lt.ne`

IsLeftCancelMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeftReflectLE_of_mulLeftReflectLT` 📖	mathematical	—	`MulLeftReflectLE` `Preorder.toLE` `PartialOrder.toPreorder`	—	`contravariant_le_iff_contravariant_lt_and_eq` `ContravariantClass.elim` `mul_left_cancel`
`mulLeftStrictMono_of_mulLeftMono` 📖	mathematical	—	`MulLeftStrictMono` `Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.lt_of_ne` `CovariantClass.elim` `LT.lt.le` `mul_ne_mul_right` `LT.lt.ne`

IsRightCancelAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addRightReflectLE_of_addRightReflectLT` 📖	mathematical	—	`AddRightReflectLE` `Preorder.toLE` `PartialOrder.toPreorder`	—	`contravariant_le_iff_contravariant_lt_and_eq` `ContravariantClass.elim` `add_right_cancel`
`addRightStrictMono_of_addRightMono` 📖	mathematical	—	`AddRightStrictMono` `Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.lt_of_ne` `CovariantClass.elim` `LT.lt.le` `add_ne_add_left` `LT.lt.ne`

IsRightCancelMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulRightReflectLE_of_mulRightReflectLT` 📖	mathematical	—	`MulRightReflectLE` `Preorder.toLE` `PartialOrder.toPreorder`	—	`contravariant_le_iff_contravariant_lt_and_eq` `ContravariantClass.elim` `mul_right_cancel`
`mulRightStrictMono_of_mulRightMono` 📖	mathematical	—	`MulRightStrictMono` `Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.lt_of_ne` `CovariantClass.elim` `LT.lt.le` `mul_ne_mul_left` `LT.lt.ne`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covariant_of_const` 📖	—	`Monotone`	—	—	`comp` `Covariant.monotone_of_const`
`covariant_of_const'` 📖	—	`Monotone`	—	—	`covariant_of_const`

(root)

Definitions

Name	Category	Theorems
`AddLeftMono` 📖	MathDef	32 math math: `PNat.addLeftMono`, `Finset.instAddLeftMono`, `WithBot.addLeftMono`, `SetTheory.Game.addLeftMono`, `SetTheory.PGame.addLeftMono`, `Finsupp.Lex.addLeftMono`, `Set.instAddLeftMono`, `Rat.instAddLeftMono`, `NNReal.addLeftMono`, `Filter.addLeftMono`, `OrderDual.addLeftMono`, `addLeftMono_of_addLeftStrictMono`, `Positive.addLeftMono`, `Multiset.instAddLeftMono`, `Tropical.addLeftMono`, `MeasureTheory.Lp.instAddLeftMono`, `MeasureTheory.VectorMeasure.instAddLeftMono`, `NatOrdinal.instAddLeftMono`, `Cardinal.addLeftMono`, `WithZero.addLeftMono`, `DFinsupp.Lex.addLeftMono`, `Finsupp.Colex.addLeftMono`, `CanonicallyOrderedAdd.toAddLeftMono`, `CompactlySupportedContinuousMap.instAddLeftMono`, `Ordinal.instAddLeftMono`, `AddQuantale.instAddLeftMono`, `WithTop.addLeftMono`, `Int.instAddLeftMono`, `DFinsupp.Colex.addLeftMono`, `SetSemiring.addLeftMono`, `IsOrderedAddMonoid.toAddLeftMono`, `ProbabilityTheory.Kernel.instAddLeftMono`
`AddLeftReflectLE` 📖	MathDef	10 math math: `NatOrdinal.instAddLeftReflectLE`, `AddGroup.addLeftReflectLE_of_addLeftMono`, `Positive.addLeftReflectLE`, `PNat.addLeftReflectLE`, `IsOrderedCancelAddMonoid.toAddLeftReflectLE`, `Finsupp.addLeftReflectLE`, `Ordinal.instAddLeftReflectLE`, `OrderDual.addLeftReflectLE`, `Multiset.instAddLeftReflectLE`, `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT`
`AddLeftReflectLT` 📖	MathDef	11 math math: `addLeftReflectLT_of_addLeftMono`, `WithBot.addLeftReflectLT`, `PNat.addLeftReflectLT`, `ENNReal.addLeftReflectLT`, `WithTop.addLeftReflectLT`, `Ordinal.instAddLeftReflectLT`, `NNReal.addLeftReflectLT`, `Positive.addLeftReflectLT`, `IsOrderedCancelAddMonoid.toAddLeftReflectLT`, `AddGroup.addLeftReflectLT_of_addLeftStrictMono`, `OrderDual.addLeftReflectLT`
`AddLeftStrictMono` 📖	MathDef	11 math math: `Finsupp.Colex.addLeftStrictMono`, `Positive.addLeftStrictMono`, `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono`, `Ordinal.instAddLeftStrictMono`, `addLeftStrictMono_of_addLeftReflectLE`, `NatOrdinal.instAddLeftStrictMono`, `Finsupp.Lex.addLeftStrictMono`, `SetTheory.PGame.addLeftStrictMono`, `SetTheory.Game.addLeftStrictMono`, `OrderDual.addLeftStrictMono`, `PNat.addLeftStrictMono`
`AddRightMono` 📖	MathDef	19 math math: `WithBot.addRightMono`, `OrderDual.addRightMono`, `Ordinal.instAddRightMono`, `Filter.addRightMono`, `DFinsupp.Colex.addRightMono`, `CompactlySupportedContinuousMap.instAddRightMono`, `Finsupp.Colex.addRightMono`, `SetTheory.PGame.addRightMono`, `addRightMono_of_addLeftMono`, `Cardinal.addRightMono`, `addRightMono_of_addRightStrictMono`, `SetTheory.Game.addRightMono`, `DFinsupp.Lex.addRightMono`, `WithTop.addRightMono`, `Finset.instAddRightMono`, `Finsupp.Lex.addRightMono`, `Set.instAddRightMono`, `IsOrderedAddMonoid.toAddRightMono`, `AddQuantale.instAddRightMono`
`AddRightReflectLE` 📖	MathDef	5 math math: `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT`, `Positive.addRightReflectLE`, `AddGroup.addRightReflectLE_of_addRightMono`, `OrderDual.addRightReflectLE`, `addRightReflectLE_of_addLeftReflectLE`
`AddRightReflectLT` 📖	MathDef	9 math math: `addRightReflectLT_of_addLeftReflectLT`, `WithTop.addRightReflectLT`, `IsOrderedCancelAddMonoid.toAddRightReflectLT`, `Positive.addRightReflectLT`, `OrderDual.addRightReflectLT`, `addRightReflectLT_of_addRightMono`, `AddGroup.addRightReflectLT_of_addRightStrictMono`, `WithBot.addRightReflectLT`, `Ordinal.instAddRightReflectLT`
`AddRightStrictMono` 📖	MathDef	9 math math: `IsRightCancelAdd.addRightStrictMono_of_addRightMono`, `addRightStrictMono_of_addRightReflectLE`, `Finsupp.Colex.addRightStrictMono`, `SetTheory.PGame.addRightStrictMono`, `SetTheory.Game.addRightStrictMono`, `Finsupp.Lex.addRightStrictMono`, `OrderDual.addRightStrictMono`, `Positive.addRightStrictMono`, `addRightStrictMono_of_addLeftStrictMono`
`Contravariant` 📖	MathDef	9 math math: `Group.covariant_swap_iff_contravariant_swap`, `contravariant_flip_iff`, `Group.covariant_iff_contravariant`, `covariant_le_iff_contravariant_lt`, `covariant_lt_iff_contravariant_le`, `contravariant_le_iff_contravariant_lt_and_eq`, `AddGroup.covariant_swap_iff_contravariant_swap`, `ContravariantClass.elim`, `AddGroup.covariant_iff_contravariant`
`ContravariantClass` 📖	CompData	22 math math: `MulPosReflectLT.toContravariantClass`, `AddGroup.covconv`, `PosMulReflectLT.toContravariantClass`, `MulPosReflectLE.toContravariantClass`, `mulPosReflectLT_iff`, `PosMulReflectLT.to_contravariantClass_pos_mul_lt`, `posMulReflectLT_iff_contravariant_pos`, `posMulReflectLT_iff`, `contravariant_le_of_contravariant_eq_and_lt`, `contravariant_lt_of_covariant_le`, `contravariant_swap_mul_of_contravariant_mul`, `AddGroup.covconv_swap`, `PosMulReflectLE.toContravariantClass`, `mulPosReflectLE_iff`, `instContravariantClassHVAddLeOfIsOrderedCancelVAdd`, `posMulReflectLE_iff`, `Group.covconv_swap`, `contravariant_swap_add_of_contravariant_add`, `mulPosReflectLT_iff_contravariant_pos`, `Group.covconv`, `instContravariantClassHSMulLeOfIsOrderedCancelSMul`, `MulPosReflectLT.to_contravariantClass_pos_mul_lt`
`Covariant` 📖	MathDef	8 math math: `Group.covariant_swap_iff_contravariant_swap`, `Group.covariant_iff_contravariant`, `covariant_le_iff_contravariant_lt`, `covariant_lt_iff_contravariant_le`, `CovariantClass.elim`, `AddGroup.covariant_swap_iff_contravariant_swap`, `AddGroup.covariant_iff_contravariant`, `covariant_flip_iff`
`CovariantClass` 📖	CompData	33 math math: `MulPosMono.to_covariantClass_nonneg_mul_le`, `covariant_lt_of_covariant_le_of_contravariant_eq`, `Filter.covariant_div`, `posMulMono_iff_covariant_pos`, `Subgroup.instCovariantClassHSMulLe`, `mulPosMono_iff_covariant_pos`, `Ideal.instCovariantClassHSMulLe`, `covariant_swap_add_of_covariant_add`, `Filter.covariant_swap_div`, `Subalgebra.instCovariantClassHSMulLe`, `covariantClass_le_of_lt`, `Submodule.instCovariantClassHSMulLe`, `Subring.instCovariantClassHSMulLe`, `PosMulStrictMono.to_covariantClass_pos_mul_le`, `Submodule.instCovariantClassHSMulLe_1`, `Subsemiring.instCovariantClassHSMulLe`, `Filter.covariant_vadd`, `Filter.covariant_sub`, `Submonoid.instCovariantClassHSMulLe`, `Filter.covariant_smul`, `covariant_lt_of_contravariant_le`, `Filter.covariant_vadd_filter`, `ValuationSubring.instCovariantClassHSMulLe`, `MulPosMono.to_covariantClass_pos_mul_le`, `covariant_swap_mul_of_covariant_mul`, `Filter.covariant_smul_filter`, `instCovariantClassHVAddLeOfIsOrderedVAdd`, `MulPosStrictMono.to_covariantClass_pos_mul_le`, `Submodule.instCovariantClassSetHSMulLe`, `PosMulMono.to_covariantClass_pos_mul_le`, `PosMulMono.to_covariantClass_nonneg_mul_le`, `instCovariantClassHSMulLeOfIsOrderedSMul`, `Filter.covariant_swap_sub`
`MulLeftMono` 📖	MathDef	20 math math: `CanonicallyOrderedMul.toMulLeftMono`, `Language.instMulLeftMono`, `SetSemiring.mulLeftMono`, `IdemSemiring.toMulLeftMono`, `Submodule.instMulLeftMono`, `Nat.instMulLeftMono`, `WithZero.instMulLeftMono`, `Filter.mulLeftMono`, `CanonicallyOrderedAdd.toMulLeftMono`, `OrderDual.mulLeftMono`, `Ordinal.mulLeftMono`, `Finset.instMulLeftMono`, `mulLeftMono_of_mulLeftStrictMono`, `Set.instMulLeftMono`, `FractionalIdeal.instMulLeftMono`, `NNReal.mulLeftMono`, `Quantale.instMulLeftMono`, `CompactlySupportedContinuousMap.instMulLeftMono`, `Tropical.mulLeftMono`, `IsOrderedMonoid.toMulLeftMono`
`MulLeftReflectLE` 📖	MathDef	4 math math: `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT`, `OrderDual.mulLeftReflectLE`, `Group.mulLeftReflectLE_of_mulLeftMono`, `IsOrderedCancelMonoid.toMulLeftReflectLE`
`MulLeftReflectLT` 📖	MathDef	5 math math: `OrderDual.mulLeftReflectLT`, `mulLeftReflectLT_of_mulLeftMono`, `WithZero.instMulLeftReflectLT`, `Group.mulLeftReflectLT_of_mulLeftStrictMono`, `IsOrderedCancelMonoid.toMulLeftReflectLT`
`MulLeftStrictMono` 📖	MathDef	4 math math: `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono`, `OrderDual.mulLeftStrictMono`, `Tropical.mulLeftStrictMono`, `mulLeftStrictMono_of_mulLeftReflectLE`
`MulRightMono` 📖	MathDef	17 math math: `mulRightMono_of_mulRightStrictMono`, `IsOrderedMonoid.toMulRightMono`, `Ordinal.mulRightMono`, `SetSemiring.mulRightMono`, `Language.instMulRightMono`, `Set.instMulRightMono`, `Tropical.mulRightMono`, `mulRightMono_of_mulLeftMono`, `Finset.instMulRightMono`, `FractionalIdeal.instMulRightMono`, `OrderDual.mulRightMono`, `CompactlySupportedContinuousMap.instMulRightMono`, `Quantale.instMulRightMono`, `Submodule.instMulRightMono`, `CanonicallyOrderedAdd.toMulRightMono`, `Filter.mulRightMono`, `IdemSemiring.toMulRightMono`
`MulRightReflectLE` 📖	MathDef	4 math math: `mulRightReflectLE_of_mulLeftReflectLE`, `Group.mulRightReflectLE_of_mulRightMono`, `IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT`, `OrderDual.mulRightReflectLE`
`MulRightReflectLT` 📖	MathDef	5 math math: `IsOrderedCancelMonoid.toMulRightReflectLT`, `mulRightReflectLT_of_mulRightMono`, `mulRightReflectLT_of_mulLeftReflectLT`, `Group.mulRightReflectLT_of_mulRightStrictMono`, `OrderDual.mulRightReflectLT`
`MulRightStrictMono` 📖	MathDef	5 math math: `Tropical.mulRightStrictMono`, `mulRightStrictMono_of_mulLeftStrictMono`, `mulRightStrictMono_of_mulRightReflectLE`, `OrderDual.mulRightStrictMono`, `IsRightCancelMul.mulRightStrictMono_of_mulRightMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`act_rel_act_of_rel` 📖	—	—	—	—	`CovariantClass.elim`
`act_rel_act_of_rel_of_rel` 📖	—	—	—	—	`trans` `act_rel_act_of_rel`
`act_rel_of_act_rel_of_rel_act_rel` 📖	—	—	—	—	`trans` `rel_of_act_rel_act`
`act_rel_of_rel_of_act_rel` 📖	—	—	—	—	`trans` `act_rel_act_of_rel`
`addLeftMono_of_addLeftStrictMono` 📖	mathematical	—	`AddLeftMono` `Preorder.toLE` `PartialOrder.toPreorder`	—	`covariantClass_le_of_lt`
`addLeftReflectLT_of_addLeftMono` 📖	mathematical	—	`AddLeftReflectLT` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`contravariant_lt_of_covariant_le`
`addLeftStrictMono_of_addLeftReflectLE` 📖	mathematical	—	`AddLeftStrictMono` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_lt_of_contravariant_le`
`addRightMono_of_addLeftMono` 📖	mathematical	—	`AddRightMono` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`covariant_swap_add_of_covariant_add`
`addRightMono_of_addRightStrictMono` 📖	mathematical	—	`AddRightMono` `Preorder.toLE` `PartialOrder.toPreorder`	—	`covariantClass_le_of_lt`
`addRightReflectLE_of_addLeftReflectLE` 📖	mathematical	—	`AddRightReflectLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`contravariant_swap_add_of_contravariant_add`
`addRightReflectLT_of_addLeftReflectLT` 📖	mathematical	—	`AddRightReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`contravariant_swap_add_of_contravariant_add`
`addRightReflectLT_of_addRightMono` 📖	mathematical	—	`AddRightReflectLT` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`contravariant_lt_of_covariant_le`
`addRightStrictMono_of_addLeftStrictMono` 📖	mathematical	—	`AddRightStrictMono` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`covariant_swap_add_of_covariant_add`
`addRightStrictMono_of_addRightReflectLE` 📖	mathematical	—	`AddRightStrictMono` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_lt_of_contravariant_le`
`contravariant_flip_iff` 📖	mathematical	—	`Contravariant`	—	—
`contravariant_le_iff_contravariant_lt_and_eq` 📖	mathematical	—	`Contravariant` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	`LE.le.lt_of_ne` `LT.lt.le` `lt_irrefl` `LE.le.antisymm` `Eq.le` `Eq.ge` `LE.le.lt_or_eq`
`contravariant_le_of_contravariant_eq_and_lt` 📖	mathematical	—	`ContravariantClass` `Preorder.toLE` `PartialOrder.toPreorder`	—	`contravariant_le_iff_contravariant_lt_and_eq` `ContravariantClass.elim`
`contravariant_lt_of_contravariant_le` 📖	mathematical	`Contravariant` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`contravariant_le_iff_contravariant_lt_and_eq`
`contravariant_lt_of_covariant_le` 📖	mathematical	—	`ContravariantClass` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_le_iff_contravariant_lt` `CovariantClass.elim`
`contravariant_swap_add_of_contravariant_add` 📖	mathematical	—	`ContravariantClass` `Function.swap` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`contravariant_flip_iff` `AddCommMagma.to_isCommutative` `ContravariantClass.elim`
`contravariant_swap_mul_of_contravariant_mul` 📖	mathematical	—	`ContravariantClass` `Function.swap` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`contravariant_flip_iff` `CommMagma.to_isCommutative` `ContravariantClass.elim`
`covariantClass_le_of_lt` 📖	mathematical	—	`CovariantClass` `Preorder.toLE` `PartialOrder.toPreorder`	—	`covariant_le_of_covariant_lt` `CovariantClass.elim`
`covariant_flip_iff` 📖	mathematical	—	`Covariant`	—	—
`covariant_le_iff_contravariant_lt` 📖	mathematical	—	`Covariant` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `Contravariant` `Preorder.toLT`	—	`not_le` `LT.lt.not_ge` `not_lt` `LE.le.not_gt`
`covariant_le_of_covariant_lt` 📖	mathematical	`Covariant` `Preorder.toLT` `PartialOrder.toPreorder`	`Preorder.toLE`	—	`LE.le.eq_or_lt` `le_rfl` `LT.lt.le`
`covariant_lt_iff_contravariant_le` 📖	mathematical	—	`Covariant` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `Contravariant` `Preorder.toLE`	—	`not_lt` `LE.le.not_gt` `not_le` `LT.lt.not_ge`
`covariant_lt_of_contravariant_le` 📖	mathematical	—	`CovariantClass` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_lt_iff_contravariant_le` `ContravariantClass.elim`
`covariant_lt_of_covariant_le_of_contravariant_eq` 📖	mathematical	—	`CovariantClass` `Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.lt_of_ne` `CovariantClass.elim` `LT.lt.le` `LT.lt.ne` `ContravariantClass.elim`
`covariant_swap_add_of_covariant_add` 📖	mathematical	—	`CovariantClass` `Function.swap` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`covariant_flip_iff` `AddCommMagma.to_isCommutative` `CovariantClass.elim`
`covariant_swap_mul_of_covariant_mul` 📖	mathematical	—	`CovariantClass` `Function.swap` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`covariant_flip_iff` `CommMagma.to_isCommutative` `CovariantClass.elim`
`instOrderedAddOfAddRightMonoOfAddRightReflectLE` 📖	mathematical	—	`Preorder.toLE` `instIsPreorder_mathlib`	—	`instIsPreorder_mathlib` `CovariantClass.elim` `ContravariantClass.elim`
`mulLeftMono_of_mulLeftStrictMono` 📖	mathematical	—	`MulLeftMono` `Preorder.toLE` `PartialOrder.toPreorder`	—	`covariantClass_le_of_lt`
`mulLeftReflectLT_of_mulLeftMono` 📖	mathematical	—	`MulLeftReflectLT` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`contravariant_lt_of_covariant_le`
`mulLeftStrictMono_of_mulLeftReflectLE` 📖	mathematical	—	`MulLeftStrictMono` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_lt_of_contravariant_le`
`mulRightMono_of_mulLeftMono` 📖	mathematical	—	`MulRightMono` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`covariant_swap_mul_of_covariant_mul`
`mulRightMono_of_mulRightStrictMono` 📖	mathematical	—	`MulRightMono` `Preorder.toLE` `PartialOrder.toPreorder`	—	`covariantClass_le_of_lt`
`mulRightReflectLE_of_mulLeftReflectLE` 📖	mathematical	—	`MulRightReflectLE` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`contravariant_swap_mul_of_contravariant_mul`
`mulRightReflectLT_of_mulLeftReflectLT` 📖	mathematical	—	`MulRightReflectLT` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`contravariant_swap_mul_of_contravariant_mul`
`mulRightReflectLT_of_mulRightMono` 📖	mathematical	—	`MulRightReflectLT` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`contravariant_lt_of_covariant_le`
`mulRightStrictMono_of_mulLeftStrictMono` 📖	mathematical	—	`MulRightStrictMono` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`covariant_swap_mul_of_covariant_mul`
`mulRightStrictMono_of_mulRightReflectLE` 📖	mathematical	—	`MulRightStrictMono` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_lt_of_contravariant_le`
`rel_act_of_act_rel_act_of_rel_act` 📖	—	—	—	—	`trans` `rel_of_act_rel_act`
`rel_act_of_rel_of_rel_act` 📖	—	—	—	—	`trans` `act_rel_act_of_rel`
`rel_iff_cov` 📖	—	—	—	—	`ContravariantClass.elim` `CovariantClass.elim`
`rel_of_act_rel_act` 📖	—	—	—	—	`ContravariantClass.elim`

---

← Back to Index