Archimedean

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

Statistics

Metric	Count
Definitions addValuation, instAdd, instAddCommMagma, instAddCommMonoid, instLinearOrderedAddCommGroupWithTop, instLinearOrderedAddCommMonoidWithTop, instNeg, instSMulInt, instSMulNat, instZero	10
Theorems addValuation_apply, add_left_cancel_of_ne_top, add_right_cancel_of_ne_top, eq_zero_or_top_of_archimedean, exists_int_ge_of_mk_nonneg, exists_int_gt_of_mk_nonneg, exists_int_le_of_mk_nonneg, exists_int_lt_of_mk_nonneg, exists_nat_ge_of_mk_nonneg, exists_nat_gt_of_mk_nonneg, instIsOrderedAddMonoid, isAddRegular_mk, lt_of_neg_of_archimedean, lt_of_pos_of_archimedean, mk_div, mk_eq_zero_of_archimedean, mk_intCast, mk_intCast_nonneg, mk_inv, mk_le_add_mk_of_archimedean, mk_le_mk_add_of_archimedean, mk_le_mk_iff_denselyOrdered, mk_le_mk_iff_ratCast, mk_map_nonneg_of_archimedean, mk_map_of_archimedean, mk_map_of_archimedean', mk_mul, mk_natCast, mk_natCast_nonneg, mk_nonneg_of_le_of_le_of_archimedean, mk_ofNat, mk_one, mk_pow, mk_ratCast, mk_ratCast_nonneg, mk_zpow, orderHom_zero, top_ne_zero, zero_ne_top	39
Total	49

ArchimedeanClass

Definitions

Name	Category	Theorems
addValuation 📖	CompOp	12 math math: FiniteResidueField.mk_eq_zero, FiniteElement.val_add, FiniteElement.not_isUnit_iff_mk_pos, FiniteElement.val_mul, FiniteElement.val_sub, FiniteResidueField.mk_eq_mk, FiniteElement.val_zero, FiniteElement.isUnit_iff_mk_eq_zero, FiniteResidueField.mk_ne_zero, FiniteElement.val_one, addValuation_apply, FiniteElement.ext_iff
instAdd 📖	CompOp	4 math math: isAddRegular_mk, mk_mul, mk_le_mk_add_of_archimedean, mk_le_add_mk_of_archimedean
instAddCommMagma 📖	CompOp	—
instAddCommMonoid 📖	CompOp	2 math math: instIsOrderedAddMonoid, FiniteElement.mk_mul_mk
instLinearOrderedAddCommGroupWithTop 📖	CompOp	12 math math: FiniteResidueField.mk_eq_zero, FiniteElement.val_add, FiniteElement.not_isUnit_iff_mk_pos, FiniteElement.val_mul, FiniteElement.val_sub, FiniteResidueField.mk_eq_mk, FiniteElement.val_zero, FiniteElement.isUnit_iff_mk_eq_zero, FiniteResidueField.mk_ne_zero, FiniteElement.val_one, mk_div, FiniteElement.ext_iff
instLinearOrderedAddCommMonoidWithTop 📖	CompOp	12 math math: FiniteResidueField.mk_eq_zero, FiniteElement.val_add, FiniteElement.not_isUnit_iff_mk_pos, FiniteElement.val_mul, FiniteElement.val_sub, FiniteResidueField.mk_eq_mk, FiniteElement.val_zero, FiniteElement.isUnit_iff_mk_eq_zero, FiniteResidueField.mk_ne_zero, FiniteElement.val_one, addValuation_apply, FiniteElement.ext_iff
instNeg 📖	CompOp	1 math math: mk_inv
instSMulInt 📖	CompOp	1 math math: mk_zpow
instSMulNat 📖	CompOp	1 math math: mk_pow
instZero 📖	CompOp	30 math math: mk_intCast, FiniteResidueField.mk_eq_zero, mk_natCast, Hyperreal.archimdeanClassMk_coe, mk_ofNat, FiniteElement.not_isUnit_iff_mk_pos, Hyperreal.archimedeanClassMk_neg_of_tendsto_atBot, orderHom_zero, mk_map_nonneg_of_archimedean, Hyperreal.archimedeanClassMk_neg_of_tendsto_atTop, mk_natCast_nonneg, Hyperreal.archimedeanClassMk_pos_of_tendsto, Hyperreal.archimedeanClassMk_nonneg_of_tendsto, FiniteResidueField.mk_eq_mk, stdPart_monotoneOn, mk_ratCast, FiniteElement.isUnit_iff_mk_eq_zero, FiniteResidueField.mk_ne_zero, mk_intCast_nonneg, Hyperreal.archimedeanClassMk_omega_neg, Hyperreal.archimedeanClassMk_coe_nonneg, mk_ratCast_nonneg, Hyperreal.tendsto_atBot_iff, mk_nonneg_of_le_of_le_of_archimedean, mk_one, eq_zero_or_top_of_archimedean, mk_eq_zero_of_archimedean, mk_map_of_archimedean', Hyperreal.archimedeanClassMk_epsilon_pos, Hyperreal.tendsto_atTop_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addValuation_apply 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ArchimedeanClass Ring.toAddCommGroup IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing instLinearOrderedAddCommMonoidWithTop AddValuation.instFunLike addValuation	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
add_left_cancel_of_ne_top 📖	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing instAdd	—	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing ind le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono nsmul_eq_mul mul_comm abs_mul IsOrderedAddMonoid.toAddLeftMono
add_right_cancel_of_ne_top 📖	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing instAdd	—	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_left_cancel_of_ne_top add_comm
eq_zero_or_top_of_archimedean 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing instZero Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instLinearOrder instOrderTop	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing ind eq_or_ne mk_eq_zero_of_archimedean
exists_int_ge_of_mk_nonneg 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero	AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing exists_nat_ge_of_mk_nonneg Int.cast_natCast
exists_int_gt_of_mk_nonneg 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero	Preorder.toLT AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing exists_nat_gt_of_mk_nonneg Int.cast_natCast
exists_int_le_of_mk_nonneg 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero	AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing exists_nat_ge_of_mk_nonneg mk_neg Int.cast_neg Int.cast_natCast IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
exists_int_lt_of_mk_nonneg 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero	Preorder.toLT AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing exists_nat_gt_of_mk_nonneg mk_neg Int.cast_neg Int.cast_natCast IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
exists_nat_ge_of_mk_nonneg 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing le_of_abs_le abs_one nsmul_eq_mul mul_one
exists_nat_gt_of_mk_nonneg 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero	Preorder.toLT AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing exists_nat_ge_of_mk_nonneg LE.le.trans_lt Nat.cast_add Nat.cast_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono contravariant_lt_of_covariant_le IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing instAddCommMonoid instLinearOrder	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing ind mk_mul le_rfl
isAddRegular_mk 📖	mathematical	—	IsAddRegular ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing instAdd	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing isAddLeftRegular_iff_isAddRegular ind nsmul_eq_mul abs_mul mul_left_comm IsOrderedRing.toPosMulMono PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono abs_pos IsOrderedAddMonoid.toAddLeftMono
lt_of_neg_of_archimedean 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLT PartialOrder.toPreorder instLinearOrder instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring OrderRingHom.instFunLike	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_of_mk_lt_mk_of_nonpos mk_map_of_archimedean' LT.lt.ne MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass OrderRingHom.instRingHomClass OrderRingHom.toRingHom_eq_coe map_zero MonoidWithZeroHomClass.toZeroHomClass OrderRingHom.monotone' LT.lt.le
lt_of_pos_of_archimedean 📖	mathematical	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLT PartialOrder.toPreorder instLinearOrder instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring OrderRingHom.instFunLike	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_of_mk_lt_mk_of_nonneg mk_map_of_archimedean' LT.lt.ne' MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass OrderRingHom.instRingHomClass OrderRingHom.toRingHom_eq_coe map_zero MonoidWithZeroHomClass.toZeroHomClass OrderRingHom.monotone' LT.lt.le
mk_div 📖	mathematical	—	Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing IsOrderedRing.toIsOrderedAddMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv DivisionRing.toDivInvMonoid ArchimedeanClass SubNegMonoid.toSub LinearOrderedAddCommGroupWithTop.toSubNegMonoid instLinearOrderedAddCommGroupWithTop	—	IsOrderedRing.toIsOrderedAddMonoid div_eq_mul_inv IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toIsStrictOrderedRing IsDomain.to_noZeroDivisors instIsDomain DivisionRing.toNontrivial mk_mul mk_inv sub_eq_add_neg
mk_eq_zero_of_archimedean 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing ArchimedeanClass instZero	—	mk_eq_mk_of_archimedean IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero
mk_intCast 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne ArchimedeanClass instZero	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing subsingleton_or_nontrivial instSubsingleton mk_map_of_archimedean' Int.instIsStrictOrderedRing instArchimedeanInt eq_intCast RingHom.instRingHomClass IsOrderedAddMonoid.toAddLeftMono IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
mk_intCast_nonneg 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing eq_or_ne Int.cast_zero mk_intCast le_refl
mk_inv 📖	mathematical	—	Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing IsOrderedRing.toIsOrderedAddMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero ArchimedeanClass instNeg	—	IsOrderedRing.toIsOrderedAddMonoid
mk_le_add_mk_of_archimedean 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instAdd DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring OrderRingHom.instFunLike	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_comm mk_le_mk_add_of_archimedean
mk_le_mk_add_of_archimedean 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instAdd DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring OrderRingHom.instFunLike	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass OrderRingHom.instRingHomClass top_add mk_map_of_archimedean' zero_add le_refl
mk_le_mk_iff_denselyOrdered 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike	ArchimedeanClass Ring.toAddCommGroup IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Preorder.toLE instLinearOrder Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass StrictMono.lt_iff_lt IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing zero_nsmul IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add abs_zero MulZeroClass.mul_zero instNontrivialOfCharZero IsStrictOrderedRing.toCharZero exists_nsmul_lt_of_pos AddGroup.existsAddOfLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid one_pos IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one le_of_mul_le_mul_left PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono nsmul_eq_mul Nat.cast_add Nat.cast_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass map_natCast map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass one_mul mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono LT.lt.le abs_nonneg Nat.cast_add_one_pos exists_lt_nsmul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd RingHom.map_zero StrictMono.monotone nsmul_nonneg mul_comm mul_assoc mul_nonneg
mk_le_mk_iff_ratCast 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing IsOrderedRing.toIsOrderedAddMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder instLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivisionRing.toRatCast abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toIsStrictOrderedRing IsDomain.to_noZeroDivisors instIsDomain DivisionRing.toNontrivial IsStrictOrderedRing.toCharZero eq_ratCast RingHom.instRingHomClass mk_le_mk_iff_denselyOrdered Rat.instIsStrictOrderedRing LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instArchimedeanRat Rat.cast_strictMono
mk_map_nonneg_of_archimedean 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring OrderRingHom.instFunLike	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_zero mk_le_mk_add_of_archimedean
mk_map_of_archimedean 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing DFunLike.coe OrderAddMonoidHom PartialOrder.toPreorder AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne OrderAddMonoidHom.instFunLike AddMonoidWithOne.toOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing mk_eq_zero_of_archimedean orderHom_zero
mk_map_of_archimedean' 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring PartialOrder.toPreorder OrderRingHom.instFunLike ArchimedeanClass instZero	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass OrderRingHom.instRingHomClass mk_map_of_archimedean
mk_mul 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ArchimedeanClass instAdd	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
mk_natCast 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne ArchimedeanClass instZero	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Nat.cast_zero Int.instCharZero Int.cast_natCast mk_intCast
mk_natCast_nonneg 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Int.cast_natCast mk_intCast_nonneg
mk_nonneg_of_le_of_le_of_archimedean 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring OrderRingHom.instFunLike	ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instLinearOrder instZero	—	LE.le.trans' IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing min_le_mk_of_le_of_le
mk_ofNat 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing ArchimedeanClass instZero	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Int.cast_natCast mk_intCast Nat.cast_zero Int.instCharZero Nat.AtLeastTwo.toNeZero
mk_one 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne ArchimedeanClass instZero	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
mk_pow 📖	mathematical	—	Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ArchimedeanClass instSMulNat	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
mk_ratCast 📖	mathematical	—	Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing IsOrderedRing.toIsOrderedAddMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivisionRing.toRatCast ArchimedeanClass instZero Field.toCommRing IsOrderedRing.toIsStrictOrderedRing IsDomain.to_noZeroDivisors instIsDomain DivisionRing.toNontrivial	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toIsStrictOrderedRing IsDomain.to_noZeroDivisors instIsDomain DivisionRing.toNontrivial IsStrictOrderedRing.toCharZero eq_ratCast RingHom.instRingHomClass Rat.cast_one mk_map_of_archimedean Rat.instIsStrictOrderedRing instArchimedeanRat
mk_ratCast_nonneg 📖	mathematical	—	ArchimedeanClass Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing IsOrderedRing.toIsOrderedAddMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder instLinearOrder instZero Field.toCommRing IsOrderedRing.toIsStrictOrderedRing IsDomain.to_noZeroDivisors instIsDomain DivisionRing.toNontrivial DivisionRing.toRatCast	—	IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toIsStrictOrderedRing IsDomain.to_noZeroDivisors instIsDomain DivisionRing.toNontrivial eq_or_ne Rat.cast_zero mk_ratCast le_refl
mk_zpow 📖	mathematical	—	Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing IsOrderedRing.toIsOrderedAddMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toZPow DivisionRing.toDivInvMonoid ArchimedeanClass instSMulInt	—	IsOrderedRing.toIsOrderedAddMonoid
orderHom_zero 📖	mathematical	—	DFunLike.coe OrderHom ArchimedeanClass Ring.toAddCommGroup CommRing.toRing IsOrderedRing.toIsOrderedAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing PartialOrder.toPreorder instLinearOrder OrderHom.instFunLike orderHom instZero OrderAddMonoidHom AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne OrderAddMonoidHom.instFunLike AddMonoidWithOne.toOne	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing mk_one
top_ne_zero 📖	—	—	—	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing NeZero.charZero_one IsStrictOrderedRing.toCharZero
zero_ne_top 📖	—	—	—	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing top_ne_zero

---

← Back to Index