ArchimedeanDensely

📁 Source: Mathlib/GroupTheory/ArchimedeanDensely.lean

Statistics

Metric	Count
Definitions closure_equiv_closure, int_orderAddMonoidIso_of_isLeast_pos, closure_equiv_closure, multiplicative_int_orderMonoidIso_of_isLeast_one_lt, instFintypeAddEquivInt, instLocallyFiniteOrderAdditive, instLocallyFiniteOrderMultiplicative, instLocallyFiniteOrderUnits, instLocallyFiniteOrderUnitsWithZero, instUniqueOrderAddMonoidIsoInt, instUniqueOrderAddMonoidIsoIntOrderDual	11
Theorems isLeast_of_closure_iff_eq_abs, mem_closure_singleton_iff_existsUnique_zsmul, of_locallyFiniteOrder, addEquiv_eq_refl_or_neg, card_fintype_addEquiv, not_denselyOrdered, univ_addEquiv, discrete_iff_not_denselyOrdered, discrete_or_denselyOrdered, isAddCyclic_iff_not_denselyOrdered, wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete, wellFoundedOn_setOf_le_lt_iff_nonempty_discrete, discrete_iff_not_denselyOrdered, discrete_or_denselyOrdered, isCyclic_iff_not_denselyOrdered, wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete, wellFoundedOn_setOf_le_lt_iff_nonempty_discrete, discrete_iff_not_denselyOrdered, discrete_or_denselyOrdered, wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero, of_locallyFiniteOrder, addArchimedean, mulArchimedean, isLeast_of_closure_iff_eq_mabs, mem_closure_singleton_iff_existsUnique_zpow, mulArchimedean_iff, denselyOrdered_iff, denselyOrdered_set_iff_subsingleton, mulArchimedean_iff, denselyOrdered_additive_iff, denselyOrdered_multiplicative_iff, exists_pow_lt₀, instDenselyOrderedAdditive, instDenselyOrderedMultiplicative, instDenselyOrderedWithZeroOfNoMinOrder, instWellFoundedGTWithZeroMultiplicativeIntLeOne, not_denselyOrdered_withZero_int	38
Total	49

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeast_of_closure_iff_eq_abs 📖	mathematical	—	IsLeast Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike closure Set Set.instSingletonSet Preorder.toLT NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid abs	—	cyclic_of_min mem_closure_singleton_self mem_closure_singleton mul_zsmul one_zsmul Int.mul_eq_one_iff_eq_one_or_neg_one sup_of_le_left neg_le_self_iff LT.lt.le neg_zsmul neg_neg sup_of_le_right sup_eq_left LE.le.trans neg_nonpos IsOrderedAddMonoid.toAddLeftMono abs.eq_1 mul_zsmul' one_mul zsmul_le_zsmul_iff_left zero_add Mathlib.Tactic.Contrapose.contrapose₁ not_lt Left.nonneg_neg_iff zsmul_nonneg closure_singleton_neg abs_neg le_of_not_ge
mem_closure_singleton_iff_existsUnique_zsmul 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike closure Set Set.instSingletonSet ExistsUnique SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	mem_closure_singleton Ne.lt_or_gt StrictAnti.injective zsmul_left_strictAnti StrictMono.injective zsmul_left_strictMono ExistsUnique.exists

Archimedean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_locallyFiniteOrder 📖	mathematical	—	Archimedean AddCommGroup.toAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	comap instArchimedeanInt LocallyFiniteOrder.orderAddMonoidHom_strictMono

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquiv_eq_refl_or_neg 📖	mathematical	—	AddEquiv.refl AddEquiv.neg AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	not_isOfFinAddOrder_of_isAddTorsionFree instIsAddTorsionFree AddEquiv.map_ne_zero_iff AddSubgroup.zmultiples_eq_zmultiples_iff zmultiples_one AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddSubgroup.map_equiv_top AddMonoidHom.map_zmultiples
card_fintype_addEquiv 📖	mathematical	—	Fintype.card AddEquiv instFintypeAddEquivInt	—	—
not_denselyOrdered 📖	mathematical	—	DenselyOrdered	—	LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered instIsOrderedAddMonoid instArchimedeanInt
univ_addEquiv 📖	mathematical	—	Finset.univ AddEquiv instFintypeAddEquivInt Finset.cons AddEquiv.neg AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Finset Finset.instSingleton AddEquiv.refl	—	—

LinearOrderedAddCommGroup

Definitions

Name	Category	Theorems
closure_equiv_closure 📖	CompOp	—
int_orderAddMonoidIso_of_isLeast_pos 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discrete_iff_not_denselyOrdered 📖	mathematical	—	OrderAddMonoidIso PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLatticeInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid DenselyOrdered Preorder.toLT	—	exists_between denselyOrdered_iff_of_orderIsoClass OrderAddMonoidIso.instOrderIsoClass one_pos Int.instZeroLEOneClass discrete_or_denselyOrdered
discrete_or_denselyOrdered 📖	mathematical	—	OrderAddMonoidIso PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLatticeInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid DenselyOrdered Preorder.toLT	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
isAddCyclic_iff_not_denselyOrdered 📖	mathematical	—	IsAddCyclic SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DenselyOrdered Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	discrete_iff_not_denselyOrdered isAddCyclic_iff_nonempty_equiv_int
wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete 📖	mathematical	—	Set.WellFoundedOn setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT OrderAddMonoidIso instLatticeInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	wellFoundedOn_setOf_le_lt_iff_nonempty_discrete Set.WellFoundedOn.mono' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Set.WellFoundedOn.mapsTo
wellFoundedOn_setOf_le_lt_iff_nonempty_discrete 📖	mathematical	—	Set.WellFoundedOn setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT OrderAddMonoidIso instLatticeInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	discrete_iff_not_denselyOrdered exists_ne le_rfl WellFounded.wellFounded_iff_has_min LT.lt.le exists_between IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono lt_of_le_of_ne Mathlib.Tactic.Push.not_forall_eq sub_nonneg covariant_swap_add_of_covariant_add Set.range_nonempty add_smul one_smul IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd contravariant_lt_of_covariant_le OrderAddMonoidIso.instOrderIsoClass BddBelow.wellFoundedOn_lt Set.WellFoundedOn.mono' contravariant_swap_add_of_contravariant_add Set.WellFoundedOn.mapsTo IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT

LinearOrderedCommGroup

Definitions

Name	Category	Theorems
closure_equiv_closure 📖	CompOp	—
multiplicative_int_orderMonoidIso_of_isLeast_one_lt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discrete_iff_not_denselyOrdered 📖	mathematical	—	OrderMonoidIso Multiplicative PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Multiplicative.preorder instLatticeInt MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Multiplicative.mul DenselyOrdered Preorder.toLT	—	Equiv.nonempty_congr LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered Additive.isOrderedAddMonoid Additive.instArchimedean denselyOrdered_iff_of_orderIsoClass OrderIso.instOrderIsoClass
discrete_or_denselyOrdered 📖	mathematical	—	OrderMonoidIso Multiplicative PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Multiplicative.preorder instLatticeInt MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Multiplicative.mul DenselyOrdered Preorder.toLT	—	Equiv.nonempty_congr LinearOrderedAddCommGroup.discrete_or_denselyOrdered Additive.isOrderedAddMonoid Additive.instArchimedean
isCyclic_iff_not_denselyOrdered 📖	mathematical	—	IsCyclic DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup DenselyOrdered Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isAddCyclic_additive_iff LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered Additive.isOrderedAddMonoid Additive.instArchimedean Additive.instNontrivial
wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete 📖	mathematical	—	Set.WellFoundedOn setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT OrderMonoidIso Multiplicative Multiplicative.preorder instLatticeInt MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Multiplicative.mul	—	wellFoundedOn_setOf_le_lt_iff_nonempty_discrete Set.WellFoundedOn.mono' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul Set.WellFoundedOn.mapsTo
wellFoundedOn_setOf_le_lt_iff_nonempty_discrete 📖	mathematical	—	Set.WellFoundedOn setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT OrderMonoidIso Multiplicative Multiplicative.preorder instLatticeInt MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Multiplicative.mul	—	Set.WellFoundedOn.mono' Set.WellFoundedOn.mapsTo OrderIso.le_symm_apply OrderIso.instOrderIsoClass LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete Additive.isOrderedAddMonoid Additive.instNontrivial Equiv.nonempty_congr

LinearOrderedCommGroupWithZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discrete_iff_not_denselyOrdered 📖	mathematical	—	OrderMonoidIso WithZero Multiplicative PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder toLinearOrderedCommMonoidWithZero WithZero.instPreorder Multiplicative.preorder instLatticeInt MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero toCommGroupWithZero WithZero.instMulZeroClass Multiplicative.mul DenselyOrdered Preorder.toLT	—	denselyOrdered_units_iff LinearOrderedCommGroup.discrete_iff_not_denselyOrdered Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.instMulArchimedean Nonempty.congr OrderMonoidIso.instMulEquivClass GroupWithZero.toNontrivial MulEquivClass.toMonoidWithZeroHomClass MulEquiv.instMulEquivClass WithZero.unzero.congr_simp Units.val_le_val OrderIsoClass.map_le_map_iff OrderMonoidIso.instOrderIsoClass WithZero.coe_le_coe WithZero.coe_unzero map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
discrete_or_denselyOrdered 📖	mathematical	—	OrderMonoidIso WithZero Multiplicative PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder toLinearOrderedCommMonoidWithZero WithZero.instPreorder Multiplicative.preorder instLatticeInt MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero toCommGroupWithZero WithZero.instMulZeroClass Multiplicative.mul DenselyOrdered Preorder.toLT	—	denselyOrdered_units_iff LinearOrderedCommGroup.discrete_or_denselyOrdered Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.instMulArchimedean
wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero 📖	mathematical	—	Set.WellFoundedOn setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder toLinearOrderedCommMonoidWithZero Preorder.toLT OrderMonoidIso WithZero Multiplicative WithZero.instPreorder Multiplicative.preorder instLatticeInt MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero toCommGroupWithZero WithZero.instMulZeroClass Multiplicative.mul	—	wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero Set.wellFoundedOn_sdiff_singleton instIsStrictOrderGt Set.WellFoundedOn.mono' inv_strictAnti₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono Mathlib.Tactic.Contrapose.contrapose₁ Set.WellFoundedOn.mapsTo eq_or_ne inv_zero inv_le_comm₀ inv_anti₀
wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero 📖	mathematical	—	Set.WellFoundedOn setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder toLinearOrderedCommMonoidWithZero Preorder.toLT OrderMonoidIso WithZero Multiplicative WithZero.instPreorder Multiplicative.preorder instLatticeInt MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero toCommGroupWithZero WithZero.instMulZeroClass Multiplicative.mul	—	Set.wellFoundedOn_sdiff_singleton instIsStrictOrderLt Set.WellFoundedOn.mono' Set.WellFoundedOn.mapsTo GroupWithZero.toNontrivial LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Nonempty.congr OrderMonoidIso.instMulEquivClass eq_or_ne MulEquiv.symm_map_mul map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing WithZero.instNontrivial OrderMonoidIso.instOrderIsoClass WithZero.coe_le_coe WithZero.coe_unzero

MulArchimedean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_locallyFiniteOrder 📖	mathematical	—	MulArchimedean CommGroup.toCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	comap Multiplicative.instMulArchimedean instArchimedeanInt LocallyFiniteOrder.orderMonoidHom_strictMono

OrderAddMonoidIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addArchimedean 📖	mathematical	—	Archimedean	—	map_lt_map_iff instOrderIsoClass map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass instAddEquivClass apply_symm_apply map_nsmul OrderIsoClass.map_le_map_iff Archimedean.arch

OrderMonoidIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulArchimedean 📖	mathematical	—	MulArchimedean	—	map_lt_map_iff instOrderIsoClass map_one MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass instMulEquivClass apply_symm_apply OrderIsoClass.map_le_map_iff MulArchimedean.arch

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeast_of_closure_iff_eq_mabs 📖	mathematical	—	IsLeast Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf Subgroup CommGroup.toGroup SetLike.instMembership instSetLike closure Set Set.instSingletonSet Preorder.toLT InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid mabs	—	cyclic_of_min mem_closure_singleton zpow_mul' zpow_one Int.mul_eq_one_iff_eq_one_or_neg_one sup_of_le_left LT.lt.le zpow_neg inv_inv sup_of_le_right sup_eq_left LE.le.trans inv_le_one' IsOrderedMonoid.toMulLeftMono mabs.eq_1 zpow_mul one_mul zpow_le_zpow_iff_right zero_add Mathlib.Tactic.Contrapose.contrapose₁ Left.one_le_inv_iff one_le_zpow closure_singleton_inv mabs_inv le_of_not_ge
mem_closure_singleton_iff_existsUnique_zpow 📖	mathematical	—	Subgroup CommGroup.toGroup SetLike.instMembership instSetLike closure Set Set.instSingletonSet ExistsUnique DivInvMonoid.toZPow Group.toDivInvMonoid	—	mem_closure_singleton Ne.lt_or_gt StrictAnti.injective zpow_right_strictAnti StrictMono.injective zpow_right_strictMono ExistsUnique.exists

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulArchimedean_iff 📖	mathematical	—	MulArchimedean Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero CommGroup.toCommMonoid instCommGroupUnits CommMonoidWithZero.toCommMonoid LinearOrderedCommMonoidWithZero.toCommMonoidWithZero LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instPartialOrderUnits SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	—	OrderMonoidIso.mulArchimedean WithZero.instMulArchimedean instMulArchimedean

WithZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denselyOrdered_iff 📖	mathematical	—	DenselyOrdered WithZero Preorder.toLT instPreorder	—	WithBot.denselyOrdered_iff
denselyOrdered_set_iff_subsingleton 📖	mathematical	—	DenselyOrdered Set.Elem WithZero Preorder.toLT instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Subsingleton	—	WithBot.denselyOrdered_set_iff_subsingleton
mulArchimedean_iff 📖	mathematical	—	MulArchimedean WithZero CommMonoidWithZero.toCommMonoid instCommMonoidWithZero CommGroup.toCommMonoid instPartialOrder	—	OrderMonoidIso.mulArchimedean Units.instMulArchimedean instMulArchimedean

(root)

Definitions

Name	Category	Theorems
instFintypeAddEquivInt 📖	CompOp	2 math math: Int.card_fintype_addEquiv, Int.univ_addEquiv
instLocallyFiniteOrderAdditive 📖	CompOp	—
instLocallyFiniteOrderMultiplicative 📖	CompOp	—
instLocallyFiniteOrderUnits 📖	CompOp	—
instLocallyFiniteOrderUnitsWithZero 📖	CompOp	—
instUniqueOrderAddMonoidIsoInt 📖	CompOp	—
instUniqueOrderAddMonoidIsoIntOrderDual 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denselyOrdered_additive_iff 📖	mathematical	—	DenselyOrdered Additive instLTAdditive	—	—
denselyOrdered_multiplicative_iff 📖	mathematical	—	DenselyOrdered Multiplicative instLTMultiplicative	—	—
exists_pow_lt₀ 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	Monoid.toNatPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero Units.val	—	eq_or_ne pow_one CanLift.prf instCanLiftUnitsValIsUnit exists_pow_lt Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.instMulArchimedean
instDenselyOrderedAdditive 📖	mathematical	—	DenselyOrdered Additive instLTAdditive	—	denselyOrdered_additive_iff
instDenselyOrderedMultiplicative 📖	mathematical	—	DenselyOrdered Multiplicative instLTMultiplicative	—	denselyOrdered_multiplicative_iff
instDenselyOrderedWithZeroOfNoMinOrder 📖	mathematical	—	DenselyOrdered WithZero Preorder.toLT WithZero.instPreorder	—	WithZero.denselyOrdered_iff
instWellFoundedGTWithZeroMultiplicativeIntLeOne 📖	mathematical	—	WellFoundedGT WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Preorder.toLT	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero WithZero.instNontrivialUnits Multiplicative.instNontrivial Int.instNontrivial one_ne_zero NeZero.one WithZero.instNontrivial
not_denselyOrdered_withZero_int 📖	mathematical	—	DenselyOrdered WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered WithZero.instNontrivialUnits Multiplicative.instNontrivial Int.instNontrivial WithZero.instMulArchimedean Multiplicative.instMulArchimedean instArchimedeanInt

---

← Back to Index