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 AddMonoid.toNatSMul	—	—
comap 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike	Archimedean	—	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 Monoid.toNatPow	—	—
comap 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MonoidHom.instFunLike	MulArchimedean	—	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_neg_iff_pos addLeftStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono neg_le_neg_iff covariant_swap_add_of_covariant_add neg_nsmul
instMulArchimedean 📖	mathematical	—	MulArchimedean OrderDual instCommMonoid CommGroup.toCommMonoid instPartialOrder	—	MulArchimedean.arch inv_lt_one_iff_one_lt mulLeftStrictMono IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul 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	19 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, NNReal.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	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib 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 IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 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 RightCancelSemigroup.toIsRightCancelMul contravariant_swap_mul_of_contravariant_mul contravariant_lt_of_covariant_le IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul 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 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_sub_iff_add_le' sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd 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 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 RightCancelSemigroup.toIsRightCancelMul 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 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 RightCancelSemigroup.toIsRightCancelMul 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 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 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 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 DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup DivInvMonoid.toZPow	—	covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul 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 SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toZSMul	—	sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd 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	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddGroupWithOne.toIntCast	—	exists_floor LT.lt.trans inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
exists_lt_nsmul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	AddMonoid.toNatSMul	—	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	Monoid.toNatPow	—	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 DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	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 DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	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 IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd 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	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib 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 IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd 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	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	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	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	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	AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	neg_nsmul neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd 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	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	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	uniform_continuous_npow_on_bounded sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	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	Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	inv_pow IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul 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	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	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	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	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 AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_add_iff_pos_left IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le 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	Monoid.toNatPow 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	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	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 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivisionRing.toRatCast Field.toDivisionRing	—	—	le_of_not_gt exists_rat_btwn LT.lt.not_ge
le_of_forall_rat_lt_imp_le 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivisionRing.toRatCast Field.toDivisionRing	—	—	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	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	exists_pos_add_of_lt' IsOrderedCancelAddMonoid.toAddLeftReflectLT IsStrictOrderedRing.toIsOrderedCancelAddMonoid add_comm add_one_pow_unbounded_of_pos

---

← Back to Index