Basic

📁 Source: Mathlib/Algebra/Order/Archimedean/Basic.lean

Statistics

Metric	Count
Definitions `floorRing`, `MulArchimedean`	2
Theorems `instAddArchimedean`, `instArchimedean`, `arch`, `comap`, `archimedean`, `arch`, `comap`, `instMulArchimedean`, `instArchimedean`, `instMulArchimedean`, `instAddArchimedean`, `instMulArchimedean`, `instMulArchimedean`, `instArchimedean`, `instMulArchimedean`, `add_one_pow_unbounded_of_pos`, `archimedean_iff_int_le`, `archimedean_iff_int_lt`, `archimedean_iff_nat_le`, `archimedean_iff_nat_lt`, `archimedean_iff_rat_le`, `archimedean_iff_rat_lt`, `eq_of_forall_lt_rat_iff_lt`, `eq_of_forall_rat_lt_iff_lt`, `existsUnique_add_zpow_mem_Ioc`, `existsUnique_add_zsmul_mem_Ico`, `existsUnique_add_zsmul_mem_Ioc`, `existsUnique_div_zpow_mem_Ico`, `existsUnique_mul_zpow_mem_Ico`, `existsUnique_sub_zpow_mem_Ioc`, `existsUnique_sub_zsmul_mem_Ico`, `existsUnique_sub_zsmul_mem_Ioc`, `existsUnique_zpow_near_of_one_lt`, `existsUnique_zpow_near_of_one_lt'`, `existsUnique_zsmul_near_of_pos`, `existsUnique_zsmul_near_of_pos'`, `exists_div_btwn`, `exists_floor`, `exists_int_ge`, `exists_int_gt`, `exists_int_le`, `exists_int_lt`, `exists_lt_nsmul`, `exists_lt_pow`, `exists_mem_Ico_zpow`, `exists_mem_Ioc_zpow`, `exists_nat_ge`, `exists_nat_gt`, `exists_nat_one_div_lt`, `exists_nat_pow_near`, `exists_nat_pow_near_of_lt_one`, `exists_nsmul_lt`, `exists_pos_rat_lt`, `exists_pow_btwn`, `exists_pow_btwn_of_lt_mul`, `exists_pow_lt`, `exists_pow_lt_of_lt_one`, `exists_rat_btwn`, `exists_rat_gt`, `exists_rat_lt`, `exists_rat_mem_uIoo`, `exists_rat_near`, `exists_rat_pow_btwn`, `exists_zpow_btwn_of_lt_mul`, `instArchimedeanInt`, `instArchimedeanNNRat`, `instArchimedeanNat`, `instArchimedeanRat`, `instIsCodirectedOrder`, `instIsDirectedOrder`, `instMulArchimedeanNNRat`, `le_iff_forall_lt_rat_imp_le`, `le_iff_forall_rat_lt_imp_le`, `le_of_forall_lt_rat_imp_le`, `le_of_forall_rat_lt_imp_le`, `pow_unbounded_of_one_lt`	76
Total	78

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAddArchimedean` 📖	mathematical	—	`Archimedean` `AddUnits` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `instAddCommGroupAddUnits` `instPartialOrderAddUnits`	—	`Archimedean.arch`

Additive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instArchimedean` 📖	mathematical	—	`Archimedean` `Additive` `addCommMonoid` `CommGroup.toCommMonoid` `partialOrder`	—	`MulArchimedean.arch`

Archimedean

Definitions

Name	Category	Theorems
`floorRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arch` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoid.toNSMul` `AddCommMonoid.toAddMonoid`	—	—
`comap` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike`	`Archimedean` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`map_nsmul` `AddMonoidHom.instAddMonoidHomClass` `StrictMono.le_iff_le` `arch` `map_zero` `AddMonoidHomClass.toZeroHomClass`

FloorRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`archimedean` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`archimedean_iff_int_le` `Int.le_ceil`

MulArchimedean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arch` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `Monoid.toPow` `CommMonoid.toMonoid`	—	—
`comap` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike`	`MulArchimedean` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MonoidHom.instMonoidHomClass` `StrictMono.le_iff_le` `arch` `map_one` `MonoidHomClass.toOneHomClass`

Multiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instMulArchimedean` 📖	mathematical	—	`MulArchimedean` `Multiplicative` `commMonoid` `AddCommGroup.toAddCommMonoid` `partialOrder`	—	`Archimedean.arch`

Nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instArchimedean` 📖	mathematical	—	`Archimedean` `Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Subtype.partialOrder`	—	`IsOrderedAddMonoid.toAddLeftMono` `Archimedean.arch`
`instMulArchimedean` 📖	mathematical	—	`MulArchimedean` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommSemiring.toCommMonoid` `commSemiring` `IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono` `Subtype.partialOrder`	—	`IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono` `LT.lt.le` `pow_unbounded_of_one_lt` `isStrictOrderedRing` `instArchimedean` `existsAddOfLE`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAddArchimedean` 📖	mathematical	—	`Archimedean` `OrderDual` `instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instPartialOrder`	—	`Archimedean.arch` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `neg_le_neg_iff` `covariant_swap_add_of_covariant_add` `neg_nsmul`
`instMulArchimedean` 📖	mathematical	—	`MulArchimedean` `OrderDual` `instCommMonoid` `CommGroup.toCommMonoid` `instPartialOrder`	—	`MulArchimedean.arch` `one_lt_inv'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `IsOrderedMonoid.toMulLeftMono` `inv_le_inv_iff` `covariant_swap_mul_of_covariant_mul` `inv_pow`

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instMulArchimedean` 📖	mathematical	—	`MulArchimedean` `Units` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `instCommGroupUnits` `instPartialOrderUnits`	—	`MulArchimedean.arch`

WithBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instArchimedean` 📖	mathematical	—	`Archimedean` `WithBot` `addCommMonoid` `instPartialOrder`	—	`LE.le.not_gt` `bot_le` `Archimedean.arch`

WithZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instMulArchimedean` 📖	mathematical	—	`MulArchimedean` `WithZero` `CommMonoidWithZero.toCommMonoid` `instCommMonoidWithZero` `instPartialOrder`	—	`LE.le.not_gt` `zero_le` `MulArchimedean.arch`

(root)

Definitions

Name	Category	Theorems
`MulArchimedean` 📖	CompData	18 math math: `WithZero.mulArchimedean_iff`, `OrderDual.instMulArchimedean`, `ValuativeRel.nonempty_orderIso_withZeroMul_int_iff`, `instMulArchimedeanNNRat`, `Valuation.nonempty_rankOne_iff_mulArchimedean`, `Valued.integer.mulArchimedean_mrange_of_isCompact_integer`, `OrderMonoidIso.mulArchimedean`, `ValuativeRel.isRankLeOne_iff_mulArchimedean`, `Multiplicative.instMulArchimedean`, `MulArchimedean.comap`, `SubmonoidClass.instMulArchimedean`, `Units.instMulArchimedean`, `WithZero.instMulArchimedean`, `Nonneg.instMulArchimedean`, `Units.mulArchimedean_iff`, `MulArchimedeanClass.mulArchimedean_of_mk_eq_mk`, `ValuativeRel.instMulArchimedeanValueGroupWithZeroOfIsRankLeOne`, `MulArchimedean.of_locallyFiniteOrder`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_one_pow_unbounded_of_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_le_one` `IsStrictOrderedRing.toZeroLEOneClass` `LT.lt.le` `nsmul_eq_mul` `lt_one_add` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `covariant_swap_add_of_covariant_add` `one_add_mul_le_pow_of_sq_nonneg` `pow_nonneg` `IsOrderedRing.toPosMulMono` `Nat.instAtLeastTwoHAddOfNat` `zero_le_two` `add_comm` `Archimedean.arch`
`archimedean_iff_int_le` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`archimedean_iff_int_lt` `le_of_lt` `lt_of_le_of_lt` `Int.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `lt_add_one` `Int.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Int.instAddLeftMono`
`archimedean_iff_int_lt` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`exists_int_gt` `archimedean_iff_nat_lt` `LT.lt.trans_le` `Int.cast_natCast` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`archimedean_iff_nat_le` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`archimedean_iff_nat_lt` `le_of_lt` `lt_of_le_of_lt` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `Nat.instIsOrderedAddMonoid`
`archimedean_iff_nat_lt` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`exists_nat_gt` `le_of_lt` `nsmul_eq_mul` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono`
`archimedean_iff_rat_le` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`archimedean_iff_rat_lt` `le_of_lt` `lt_of_le_of_lt` `Rat.cast_lt` `lt_add_one` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Rat.instIsStrictOrderedRing` `Rat.instAddLeftMono`
`archimedean_iff_rat_lt` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`exists_nat_gt` `Rat.cast_natCast` `archimedean_iff_nat_lt` `Rat.instIsStrictOrderedRing` `lt_of_lt_of_le` `Nat.le_ceil`
`eq_of_forall_lt_rat_iff_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	—	`LE.le.antisymm` `le_of_forall_lt_rat_imp_le` `LT.lt.le`
`eq_of_forall_rat_lt_iff_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	—	`LE.le.antisymm` `le_of_forall_rat_lt_imp_le` `LT.lt.le`
`existsUnique_add_zpow_mem_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `DivInvMonoid.toZPow`	—	`Function.Bijective.existsUnique_iff` `Equiv.bijective` `zpow_add_one` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT` `instIsRightCancelMulOfMulRightReflectLE` `contravariant_swap_mul_of_contravariant_mul` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `contravariant_lt_of_covariant_le` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `existsUnique_zpow_near_of_one_lt`
`existsUnique_add_zsmul_mem_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`Function.Bijective.existsUnique_iff` `Equiv.bijective` `add_comm` `neg_zsmul` `sub_eq_add_neg` `Set.mem_Ico` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `add_assoc` `zero_add` `existsUnique_zsmul_near_of_pos'`
`existsUnique_add_zsmul_mem_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`Function.Bijective.existsUnique_iff` `Equiv.bijective` `add_one_zsmul` `add_assoc` `Set.mem_Ioc` `add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `le_sub_iff_add_le'` `sub_lt_iff_lt_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `existsUnique_zsmul_near_of_pos`
`existsUnique_div_zpow_mem_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `DivInvMonoid.toDiv` `DivInvMonoid.toZPow`	—	`mul_comm` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `instIsRightCancelMulOfMulRightReflectLE` `contravariant_swap_mul_of_contravariant_mul` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `contravariant_lt_of_covariant_le` `mul_assoc` `one_mul` `existsUnique_zpow_near_of_one_lt'`
`existsUnique_mul_zpow_mem_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `DivInvMonoid.toZPow`	—	`Function.Bijective.existsUnique_iff` `Equiv.bijective` `mul_comm` `zpow_neg` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `instIsRightCancelMulOfMulRightReflectLE` `contravariant_swap_mul_of_contravariant_mul` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `contravariant_lt_of_covariant_le` `mul_assoc` `one_mul` `existsUnique_zpow_near_of_one_lt'`
`existsUnique_sub_zpow_mem_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `DivInvMonoid.toDiv` `DivInvMonoid.toZPow`	—	`Function.Bijective.existsUnique_iff` `Equiv.bijective` `zpow_neg` `div_inv_eq_mul` `existsUnique_add_zpow_mem_Ioc`
`existsUnique_sub_zsmul_mem_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `SubNegMonoid.toZSMul`	—	`add_comm` `Set.mem_Ico` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `add_assoc` `zero_add` `existsUnique_zsmul_near_of_pos'`
`existsUnique_sub_zsmul_mem_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ExistsUnique` `Set` `Set.instMembership` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `SubNegMonoid.toZSMul`	—	`Function.Bijective.existsUnique_iff` `Equiv.bijective` `neg_zsmul` `sub_neg_eq_add` `existsUnique_add_zsmul_mem_Ioc`
`existsUnique_zpow_near_of_one_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`ExistsUnique` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `Preorder.toLT`	—	`MulArchimedean.arch` `zpow_neg` `zpow_natCast` `inv_inv` `inv_le_inv'` `zpow_le_zpow_iff_right` `le_trans` `Int.exists_greatest_of_bdd` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `lt_add_one` `Int.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Int.instAddLeftMono` `LE.le.antisymm` `zpow_lt_zpow_iff_right` `lt_of_le_of_lt`
`existsUnique_zpow_near_of_one_lt'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`ExistsUnique` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `DivInvMonoid.toZPow` `Preorder.toLT`	—	`covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `zpow_add_one` `existsUnique_zpow_near_of_one_lt`
`existsUnique_zsmul_near_of_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ExistsUnique` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preorder.toLT`	—	`Archimedean.arch` `neg_zsmul` `natCast_zsmul` `neg_neg` `neg_le_neg` `zsmul_le_zsmul_iff_left` `le_trans` `Int.exists_greatest_of_bdd` `Mathlib.Tactic.Contrapose.contrapose₁` `not_lt` `Mathlib.Tactic.Push.not_forall_eq` `not_le` `lt_add_one` `Int.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Int.instAddLeftMono` `LE.le.antisymm` `zsmul_lt_zsmul_iff_left` `lt_of_le_of_lt`
`existsUnique_zsmul_near_of_pos'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ExistsUnique` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `Preorder.toLT`	—	`sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_lt_iff_lt_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `add_one_zsmul` `existsUnique_zsmul_near_of_pos`
`exists_div_btwn` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`exists_floor` `LT.lt.trans` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `lt_div_iff₀` `lt_iff_lt_of_le_iff_le` `lt_add_one` `Int.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `Int.instIsStrictOrderedRing` `Int.instAddLeftMono` `Int.cast_add` `Int.cast_one` `lt_imp_lt_of_le_of_le` `add_le_add_left` `le_rfl` `le_refl` `lt_sub_iff_add_lt'` `sub_mul` `div_lt_iff₀'` `one_div`
`exists_floor` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`exists_floor'` `exists_int_lt` `LT.lt.le` `exists_int_gt`
`exists_int_ge` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`exists_nat_ge` `Int.cast_natCast`
`exists_int_gt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`exists_nat_gt` `Int.cast_natCast`
`exists_int_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`exists_int_ge` `Int.cast_neg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`exists_int_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`exists_int_gt` `Int.cast_neg` `neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `covariant_swap_add_of_covariant_add`
`exists_lt_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoid.toNSMul` `AddCommMonoid.toAddMonoid`	—	`Archimedean.arch` `LE.le.trans_lt` `nsmul_lt_nsmul_left`
`exists_lt_pow` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Preorder.toLT` `PartialOrder.toPreorder` `Monoid.toPow` `CommMonoid.toMonoid`	—	`MulArchimedean.arch` `LE.le.trans_lt` `pow_lt_pow_right'`
`exists_mem_Ico_zpow` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Set` `Set.instMembership` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring`	—	`pow_unbounded_of_one_lt` `zpow_neg` `zpow_natCast` `LT.lt.le` `inv_lt_comm₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `lt_trans` `inv_pos` `Mathlib.Tactic.Contrapose.contrapose₁` `le_trans` `zpow_le_zpow_right₀` `IsStrictOrderedRing.toZeroLEOneClass` `Int.exists_greatest_of_bdd` `lt_of_not_ge` `LT.lt.not_ge`
`exists_mem_Ioc_zpow` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Set` `Set.instMembership` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring`	—	`exists_mem_Ico_zpow` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `lt_trans` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `zpow_neg` `inv_lt_comm₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `zpow_pos` `neg_add` `neg_add_cancel_right` `le_inv_comm₀`
`exists_nat_ge` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `nsmul_one` `Archimedean.arch` `one_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.one`
`exists_nat_gt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`nsmul_one` `exists_lt_nsmul` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`exists_nat_one_div_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toNatCast`	—	`exists_nat_gt` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_add_one_pos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `div_lt_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `LT.lt.trans` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le`
`exists_nat_pow_near` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Preorder.toLT`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Preorder.toLT`	—	`pow_unbounded_of_one_lt` `Nat.find_spec` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `not_le_of_gt` `pow_zero` `ne_of_gt` `le_of_not_gt` `Nat.find_min`
`exists_nat_pow_near_of_lt_one` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Preorder.toLE` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Preorder.toLE`	—	`exists_nat_pow_near` `one_le_inv_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `one_lt_inv_iff₀` `inv_lt_inv₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `inv_pow` `inv_le_inv₀`
`exists_nsmul_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`neg_nsmul` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `covariant_swap_add_of_covariant_add` `exists_lt_nsmul` `neg_pos`
`exists_pos_rat_lt` 📖	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.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`exists_rat_btwn`
`exists_pow_btwn` 📖	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.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`uniform_continuous_npow_on_bounded` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `max_lt_iff` `exists_nat_ge` `le_trans` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `LE.le.trans` `LT.lt.le` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `DivisionRing.toNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `le_self_pow₀` `IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `le_add_of_nonneg_left` `le_of_lt` `Nat.find_pos` `Nat.cast_zero` `MulZeroClass.zero_mul` `zero_pow` `lt_of_not_ge` `Nat.find_min` `LT.lt.ne'` `Eq.trans_lt` `abs_eq_self` `mul_nonneg` `Nat.cast_nonneg'` `lt_max_iff` `LE.le.trans_lt` `le_of_not_gt` `sub_sub_cancel` `sub_le_sub_right` `Nat.find_spec` `sub_lt_sub_left` `le_abs_self` `Nat.cast_succ` `sub_mul` `add_sub_cancel_left` `one_mul` `le_refl` `lt_of_le_of_ne` `LT.lt.ne` `le_sup_right` `le_sup_left`
`exists_pow_btwn_of_lt_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Preorder.toLE` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`exists_pow_lt_of_lt_one` `LT.lt.trans_le` `LT.lt.false` `LT.lt.trans` `pow_zero` `mul_lt_of_lt_one_right` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.find_min` `mul_lt_mul_iff_left₀` `IsStrictOrderedRing.toMulPosStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `pow_succ` `Nat.find_spec`
`exists_pow_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`inv_pow` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `IsOrderedMonoid.toMulLeftMono` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `instIsRightCancelMulOfMulRightReflectLE` `contravariant_swap_mul_of_contravariant_mul` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `contravariant_lt_of_covariant_le` `covariant_swap_mul_of_covariant_mul` `exists_lt_pow` `one_lt_inv'`
`exists_pow_lt_of_lt_one` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`pow_one` `LE.le.trans_lt` `pow_unbounded_of_one_lt` `one_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `inv_lt_inv₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `inv_pow`
`exists_rat_btwn` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`exists_nat_gt` `exists_div_btwn` `Rat.cast_div` `IsStrictOrderedRing.toCharZero` `Rat.cast_intCast` `Rat.cast_natCast`
`exists_rat_gt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`archimedean_iff_rat_lt`
`exists_rat_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`exists_int_lt` `Rat.cast_intCast`
`exists_rat_mem_uIoo` 📖	mathematical	—	`Set` `Set.instMembership` `Set.uIoo` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`exists_rat_btwn` `min_lt_max`
`exists_rat_near` 📖	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.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `DivisionRing.toRatCast`	—	`exists_rat_btwn` `LT.lt.trans` `sub_lt_self_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `lt_add_iff_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `covariant_swap_add_of_covariant_add` `abs_sub_lt_iff` `sub_lt_comm` `sub_lt_iff_lt_add`
`exists_rat_pow_btwn` 📖	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.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`exists_rat_btwn` `max_lt` `LE.le.trans_lt` `le_max_right` `exists_pow_btwn` `Rat.instIsStrictOrderedRing` `instArchimedeanRat` `Nat.cast_zero` `le_max_left` `LT.lt.trans` `LT.lt.trans'`
`exists_zpow_btwn_of_lt_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring`	—	`le_or_gt` `exists_pow_lt_of_lt_one` `LE.le.trans_lt` `zpow_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `zpow_natCast` `exists_pow_btwn_of_lt_mul` `lt_or_ge` `zpow_zero` `lt_inv_mul_iff₀'` `inv_mul_lt_iff₀` `inv_pos_of_pos` `inv_le_one_of_one_le₀` `zpow_neg` `lt_inv_comm₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `inv_lt_comm₀`
`instArchimedeanInt` 📖	mathematical	—	`Archimedean` `Int.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	—	`le_trans` `nsmul_eq_mul` `zero_add` `mul_one` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing`
`instArchimedeanNNRat` 📖	mathematical	—	`Archimedean` `NNRat` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`Nonneg.instArchimedean` `Rat.instIsOrderedAddMonoid` `instArchimedeanRat`
`instArchimedeanNat` 📖	mathematical	—	`Archimedean` `Nat.instAddCommMonoid` `Nat.instPartialOrder`	—	`mul_one` `nsmul_eq_mul` `Nat.cast_id`
`instArchimedeanRat` 📖	mathematical	—	`Archimedean` `Rat.addCommMonoid` `Rat.instPartialOrder`	—	`archimedean_iff_rat_le` `Rat.instIsStrictOrderedRing` `Rat.cast_id` `le_refl`
`instIsCodirectedOrder` 📖	mathematical	—	`IsCodirectedOrder` `Preorder.toLE` `PartialOrder.toPreorder`	—	`exists_int_le` `le_trans` `Int.cast_mono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `min_le_left` `min_le_right`
`instIsDirectedOrder` 📖	mathematical	—	`IsDirectedOrder` `Preorder.toLE` `PartialOrder.toPreorder`	—	`exists_nat_ge` `exists_ge_ge` `SemilatticeSup.instIsDirectedOrder` `LE.le.trans` `Nat.mono_cast` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`instMulArchimedeanNNRat` 📖	mathematical	—	`MulArchimedean` `NNRat` `CommSemiring.toCommMonoid` `instCommSemiringNNRat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`Nonneg.instMulArchimedean` `Rat.instIsStrictOrderedRing` `instArchimedeanRat` `AddGroup.existsAddOfLE`
`le_iff_forall_lt_rat_imp_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`LE.le.trans` `LT.lt.le` `le_of_forall_lt_rat_imp_le`
`le_iff_forall_rat_lt_imp_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`LE.le.trans` `LT.lt.le` `le_of_forall_rat_lt_imp_le`
`le_of_forall_lt_rat_imp_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_of_not_gt` `exists_rat_btwn` `LT.lt.not_ge`
`le_of_forall_rat_lt_imp_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_of_not_gt` `exists_rat_btwn` `LT.lt.not_ge`
`pow_unbounded_of_one_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`exists_pos_add_of_lt'` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `add_comm` `add_one_pow_unbounded_of_pos`

---

← Back to Index