Archimedean

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

Statistics

Metric	Count
Definitions Archimedean	1
Theorems dense_iff_ne_zmultiples, dense_of_no_min, dense_of_not_isolated_zero, dense_or_cyclic, dense_xor'_cyclic, denseRange_cast, dense_iff_ne_zpowers, dense_of_no_min, dense_of_not_isolated_one, dense_or_cyclic, dense_xor'_cyclic	11
Total	12

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_iff_ne_zmultiples 📖	mathematical	—	Dense SetLike.coe AddSubgroup AddCommGroup.toAddGroup instSetLike	—	xor_iff_iff_not dense_xor'_cyclic
dense_of_no_min 📖	mathematical	IsLeast Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike Preorder.toLT NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Dense SetLike.coe	—	dense_of_not_isolated_zero Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_exists Mathlib.Tactic.Push.not_and_eq exists_isLeast_pos Set.disjoint_left
dense_of_not_isolated_zero 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike Set Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Dense SetLike.coe	—	subsingleton_or_nontrivial subset_closure ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass dense_of_exists_between sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ExistsUnique.exists existsUnique_add_zsmul_mem_Ioc zsmul_mem zero_add LE.le.trans_lt lt_sub_iff_add_lt' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
dense_or_cyclic 📖	mathematical	—	Dense SetLike.coe AddSubgroup AddCommGroup.toAddGroup instSetLike closure Set Set.instSingletonSet	—	dense_of_not_isolated_zero Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_exists Mathlib.Tactic.Push.not_and_eq cyclic_of_isolated_zero Set.disjoint_left em
dense_xor'_cyclic 📖	mathematical	—	Xor' Dense SetLike.coe AddSubgroup AddCommGroup.toAddGroup instSetLike zmultiples	—	xor_true not_denseRange_zsmul zmultiples_eq_closure xor_false dense_or_cyclic

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denseRange_cast 📖	mathematical	—	DenseRange DivisionRing.toRatCast Field.toDivisionRing	—	dense_of_exists_between DivisionRing.toNontrivial Set.exists_range_iff exists_rat_btwn

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_iff_ne_zpowers 📖	mathematical	—	Dense SetLike.coe Subgroup CommGroup.toGroup instSetLike	—	xor_iff_iff_not dense_xor'_cyclic
dense_of_no_min 📖	mathematical	IsLeast Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf Subgroup CommGroup.toGroup SetLike.instMembership instSetLike Preorder.toLT InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Dense SetLike.coe	—	dense_of_not_isolated_one Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq exists_isLeast_one_lt Set.disjoint_left
dense_of_not_isolated_one 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership instSetLike Set Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Dense SetLike.coe	—	subsingleton_or_nontrivial subset_closure OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass instSubgroupClass dense_of_exists_between one_lt_div' IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ExistsUnique.exists existsUnique_add_zpow_mem_Ioc zpow_mem one_mul LE.le.trans_lt lt_div_iff_mul_lt' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul
dense_or_cyclic 📖	mathematical	—	Dense SetLike.coe Subgroup CommGroup.toGroup instSetLike closure Set Set.instSingletonSet	—	dense_of_not_isolated_one Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_eq cyclic_of_isolated_one Set.disjoint_left em
dense_xor'_cyclic 📖	mathematical	—	Xor' Dense SetLike.coe Subgroup CommGroup.toGroup instSetLike zpowers	—	xor_true not_denseRange_zpow zpowers_eq_closure xor_false dense_or_cyclic

(root)

Definitions

Name	Category	Theorems
Archimedean 📖	CompData	26 math math: Real.instArchimedean, AddUnits.instAddArchimedean, archimedean_iff_nat_le, instArchimedeanNat, OrderDual.instAddArchimedean, FloorRing.archimedean, Nonneg.instArchimedean, instArchimedeanNNRat, ConditionallyCompleteLinearOrderedField.to_archimedean, Additive.instArchimedean, archimedean_iff_nat_lt, OrderAddMonoidIso.addArchimedean, Archimedean.comap, archimedean_iff_rat_le, ArchimedeanClass.archimedean_of_mk_eq_mk, AddSubmonoidClass.instAddArchimedean, ArchimedeanClass.FiniteResidueField.instArchimedean, WithBot.instArchimedean, HahnEmbedding.ArchimedeanStrata.archimedean_stratum, archimedean_iff_int_lt, archimedean_iff_rat_lt, instArchimedeanInt, instArchimedeanRat, NNReal.instArchimedean, archimedean_iff_int_le, Archimedean.of_locallyFiniteOrder

---

← Back to Index