Structures · Algebra
Archimedean
An ordered additive commutative monoid is called Archimedean if for any two elements x, y
such that 0 < y, there exists a natural number n such that x ≤ n • y.
- Defined in
- Mathlib.Algebra.Order.Archimedean.Defs
- Shape
- One type argument · adds arch
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances12
- Int
- Nat
- Real
- Rat
- NNReal
- NNRat
- ArchimedeanClass.FiniteResidueField
- AddUnits
- Subtype
- OrderDual
- WithBot
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by655
- toIocMod
- toIcoMod
- toIocDiv
- toIcoDiv
- tendsto_natCast_atTop_atTop
- HahnEmbedding.Partial
- exists_rat_btwn
- exists_nat_gt
- toIocMod.congr_simp
- toIcoMod.congr_simp
- FiniteArchimedeanClass.ball
- tendsto_pow_atTop_atTop_of_one_lt
- toIocDiv.congr_simp
- toIcoDiv.congr_simp
- HahnEmbedding.ArchimedeanStrata.stratum
- exists_nat_ge
- Archimedean.arch
- tendsto_pow_atTop_nhds_zero_of_lt_one
- exists_pow_lt_of_lt_one
- AddCircle.liftIoc
- HahnEmbedding.Partial.eval
- AddCircle.equivIoc
- HahnEmbedding.Seed.baseEmbedding
- HahnEmbedding.Seed.toArchimedeanStrata
- AddCircle.equivIco
- exists_rat_gt
- AddCircle.liftIco
- FiniteArchimedeanClass.closedBall
- toIcoMod_mem_Ico
- HahnEmbedding.Partial.evalCoeff
- toIocDiv_eq_of_sub_zsmul_mem_Ioc
- toIocMod_mem_Ioc
- HahnEmbedding.Partial.evalCoeff_eq
- ArchimedeanClass.FiniteResidueField.ofArchimedean
- exists_nat_one_div_lt
- ArchimedeanClass.mk_map_of_archimedean'
- toIcoDiv_eq_of_sub_zsmul_mem_Ico
- existsUnique_add_zsmul_mem_Ioc
- pow_unbounded_of_one_lt
- HahnEmbedding.Seed.coeff
- sub_toIcoDiv_zsmul_mem_Ico
- toIocMod_add_zsmul
- HahnEmbedding.Partial.sSupFun
- Filter.Eventually.natCast_atTop
- toIcoDiv_add_zsmul
- ArchimedeanClass.mk_map_nonneg_of_archimedean
- Rat.denseRange_cast
- toIcoMod_add_zsmul
- toIocDiv_add_zsmul
- AddCircle.liftIoc_coe_apply
Ancestors0
No ancestors.