Ordered

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Ordered.lean

Statistics

Metric	Count
Definitions	0
Theorems left_le_lineMap_iff_le, left_le_lineMap_iff_nonneg, left_le_midpoint, left_lt_lineMap_iff_lt, left_lt_lineMap_iff_pos, lineMap_le_left_iff_le, lineMap_le_left_iff_nonpos, lineMap_le_lineMap_iff_of_lt, lineMap_le_lineMap_iff_of_lt', lineMap_le_map_iff_slope_le_slope, lineMap_le_map_iff_slope_le_slope_left, lineMap_le_map_iff_slope_le_slope_right, lineMap_le_right_iff_le, lineMap_le_right_iff_le_one, lineMap_lt_left_iff_lt, lineMap_lt_left_iff_neg, lineMap_lt_lineMap_iff_of_lt, lineMap_lt_lineMap_iff_of_lt', lineMap_lt_map_iff_slope_lt_slope, lineMap_lt_map_iff_slope_lt_slope_left, lineMap_lt_map_iff_slope_lt_slope_right, lineMap_lt_right_iff_lt, lineMap_lt_right_iff_lt_one, lineMap_mono_endpoints, lineMap_mono_left, lineMap_mono_right, lineMap_strict_mono_endpoints, lineMap_strict_mono_left, lineMap_strict_mono_right, map_le_lineMap_iff_slope_le_slope, map_le_lineMap_iff_slope_le_slope_left, map_le_lineMap_iff_slope_le_slope_right, map_lt_lineMap_iff_slope_lt_slope, map_lt_lineMap_iff_slope_lt_slope_left, map_lt_lineMap_iff_slope_lt_slope_right, midpoint_le_left, midpoint_le_midpoint, midpoint_le_right, neg_of_slope_pos, pos_of_slope_pos, right_le_lineMap_iff_le, right_le_lineMap_iff_one_le, right_le_midpoint, right_lt_lineMap_iff_lt, right_lt_lineMap_iff_one_lt, slope_pos_iff, slope_pos_iff_gt	47
Total	47

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
left_le_lineMap_iff_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Preorder.toLE DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_zero lineMap_le_lineMap_iff_of_lt
left_le_lineMap_iff_nonneg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lineMap_le_lineMap_iff_of_lt' AffineMap.lineMap_apply_zero
left_le_midpoint 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder midpoint DivisionRing.toRing Field.toDivisionRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder addGroupIsAddTorsor AddCommGroup.toAddGroup	—	left_le_lineMap_iff_le IsStrictOrderedRing.toCharZero inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono zero_lt_two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
left_lt_lineMap_iff_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_zero lineMap_lt_lineMap_iff_of_lt
left_lt_lineMap_iff_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lineMap_lt_lineMap_iff_of_lt' AffineMap.lineMap_apply_zero
lineMap_le_left_iff_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Preorder.toLE DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	left_le_lineMap_iff_le OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
lineMap_le_left_iff_nonpos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lineMap_le_lineMap_iff_of_lt' AffineMap.lineMap_apply_zero
lineMap_le_lineMap_iff_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_module le_sub_iff_add_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono add_sub_assoc sub_le_iff_le_add' sub_smul sub_sub_sub_cancel_left smul_le_smul_iff_of_pos_left IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
lineMap_le_lineMap_iff_of_lt' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	add_le_add_iff_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid smul_le_smul_iff_of_pos_right PosSMulMono.toSMulPosMono IsStrictOrderedRing.toIsOrderedRing IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule SMulPosStrictMono.toSMulPosReflectLE PosSMulStrictMono.toSMulPosStrictMono IsStrictOrderedModule.toPosSMulStrictMono sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono
lineMap_le_map_iff_slope_le_slope 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope	—	map_le_lineMap_iff_slope_le_slope OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
lineMap_le_map_iff_slope_le_slope_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope	—	map_le_lineMap_iff_slope_le_slope_left OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
lineMap_le_map_iff_slope_le_slope_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope	—	map_le_lineMap_iff_slope_le_slope_right OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
lineMap_le_right_iff_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_one lineMap_le_lineMap_iff_of_lt
lineMap_le_right_iff_le_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_le_lineMap_iff_of_lt' AffineMap.lineMap_apply_one
lineMap_lt_left_iff_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	left_lt_lineMap_iff_lt OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLT
lineMap_lt_left_iff_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lineMap_lt_lineMap_iff_of_lt' AffineMap.lineMap_apply_zero
lineMap_lt_lineMap_iff_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_module lt_sub_iff_add_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono add_sub_assoc sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_smul sub_sub_sub_cancel_left smul_lt_smul_iff_of_pos_left IsStrictOrderedModule.toPosSMulStrictMono sub_pos IsOrderedRing.toIsOrderedAddMonoid
lineMap_lt_lineMap_iff_of_lt' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid smul_lt_smul_iff_of_pos_right PosSMulStrictMono.toSMulPosStrictMono IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedModule.toPosSMulStrictMono SMulPosReflectLE.toSMulPosReflectLT SMulPosStrictMono.toSMulPosReflectLE sub_pos
lineMap_lt_map_iff_slope_lt_slope 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope	—	map_lt_lineMap_iff_slope_lt_slope OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
lineMap_lt_map_iff_slope_lt_slope_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope	—	map_lt_lineMap_iff_slope_lt_slope_left OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
lineMap_lt_map_iff_slope_lt_slope_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope	—	map_lt_lineMap_iff_slope_lt_slope_right OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
lineMap_lt_right_iff_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_one lineMap_lt_lineMap_iff_of_lt
lineMap_lt_right_iff_lt_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_lt_lineMap_iff_of_lt' AffineMap.lineMap_apply_one
lineMap_mono_endpoints 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	LE.le.trans lineMap_mono_left lineMap_mono_right
lineMap_mono_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_module add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono smul_le_smul_of_nonneg_left IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule sub_nonneg IsOrderedRing.toIsOrderedAddMonoid
lineMap_mono_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_module add_le_add_right IsOrderedAddMonoid.toAddLeftMono smul_le_smul_of_nonneg_left IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule
lineMap_strict_mono_endpoints 📖	mathematical	Preorder.toLT PartialOrder.toPreorder Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	LE.le.eq_or_lt AffineMap.lineMap_apply_zero LE.le.trans_lt lineMap_mono_left LT.lt.le lineMap_strict_mono_right
lineMap_strict_mono_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_module add_lt_add_left IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono smul_lt_smul_of_pos_left IsStrictOrderedModule.toPosSMulStrictMono sub_pos IsOrderedRing.toIsOrderedAddMonoid
lineMap_strict_mono_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	AffineMap.lineMap_apply_module add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono smul_lt_smul_of_pos_left IsStrictOrderedModule.toPosSMulStrictMono
map_le_lineMap_iff_slope_le_slope 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AffineMap.instFunLike AffineMap.lineMap AddCommGroup.toAddGroup slope	—	map_le_lineMap_iff_slope_le_slope_left mul_pos IsStrictOrderedRing.toPosMulStrictMono sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lineMap_slope_lineMap_slope_lineMap right_le_lineMap_iff_le
map_le_lineMap_iff_slope_le_slope_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AffineMap.instFunLike AffineMap.lineMap AddCommGroup.toAddGroup slope	—	AffineMap.lineMap_apply slope.eq_1 vsub_eq_sub vadd_eq_add smul_eq_mul add_sub_cancel_right smul_sub sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono mul_inv_rev SemigroupAction.mul_smul smul_add smul_smul inv_smul_le_iff_of_pos IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule mul_inv_cancel_right₀ right_ne_zero_of_mul LT.lt.ne' smul_inv_smul₀ left_ne_zero_of_mul
map_le_lineMap_iff_slope_le_slope_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AffineMap.instFunLike AffineMap.lineMap AddCommGroup.toAddGroup slope	—	AffineMap.lineMap_apply_one_sub sub_add_eq_sub_sub_swap sub_self zero_sub neg_mul_eq_mul_neg neg_sub le_inv_smul_iff_of_pos IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule smul_smul mul_inv_cancel_right₀ right_ne_zero_of_mul LT.lt.ne' le_sub_comm IsOrderedAddMonoid.toAddLeftMono smul_neg neg_add_eq_sub
map_lt_lineMap_iff_slope_lt_slope 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AffineMap.instFunLike AffineMap.lineMap AddCommGroup.toAddGroup slope	—	lt_iff_lt_of_le_iff_le' lineMap_le_map_iff_slope_le_slope map_le_lineMap_iff_slope_le_slope
map_lt_lineMap_iff_slope_lt_slope_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AffineMap.instFunLike AffineMap.lineMap AddCommGroup.toAddGroup slope	—	lt_iff_lt_of_le_iff_le' lineMap_le_map_iff_slope_le_slope_left map_le_lineMap_iff_slope_le_slope_left
map_lt_lineMap_iff_slope_lt_slope_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AffineMap.instFunLike AffineMap.lineMap AddCommGroup.toAddGroup slope	—	lt_iff_lt_of_le_iff_le' lineMap_le_map_iff_slope_le_slope_right map_le_lineMap_iff_slope_le_slope_right
midpoint_le_left 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder midpoint DivisionRing.toRing Field.toDivisionRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder addGroupIsAddTorsor AddCommGroup.toAddGroup	—	lineMap_le_left_iff_le IsStrictOrderedRing.toCharZero inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono zero_lt_two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
midpoint_le_midpoint 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	midpoint addGroupIsAddTorsor AddCommGroup.toAddGroup	—	Nat.instAtLeastTwoHAddOfNat lineMap_mono_endpoints IsStrictOrderedRing.toIsOrderedRing invOf_nonneg zero_le_two IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid invOf_le_one one_le_two
midpoint_le_right 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder midpoint DivisionRing.toRing Field.toDivisionRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder addGroupIsAddTorsor AddCommGroup.toAddGroup	—	lineMap_le_right_iff_le IsStrictOrderedRing.toCharZero two_inv_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
neg_of_slope_pos 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing slope Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—	slope_pos_iff_gt
pos_of_slope_pos 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing slope Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—	sub_zero IsStrictOrderedRing.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
right_le_lineMap_iff_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	lineMap_le_right_iff_le OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLE
right_le_lineMap_iff_one_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Preorder.toLE DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_le_lineMap_iff_of_lt' AffineMap.lineMap_apply_one
right_le_midpoint 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder midpoint DivisionRing.toRing Field.toDivisionRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder addGroupIsAddTorsor AddCommGroup.toAddGroup	—	right_le_lineMap_iff_le IsStrictOrderedRing.toCharZero two_inv_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
right_lt_lineMap_iff_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	lineMap_lt_right_iff_lt OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsStrictOrderedModule OrderDual.instPosSMulReflectLT
right_lt_lineMap_iff_one_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_lt_lineMap_iff_of_lt' AffineMap.lineMap_apply_one
slope_pos_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing slope Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	IsStrictOrderedRing.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
slope_pos_iff_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing slope Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	slope_comm slope_pos_iff

---

← Back to Index