Archimedean groups and fields. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the archimedean property for ordered groups and proves several results connected
to this notion. Being archimedean means that for all elements x
and y>0
there exists a natural
number n
such that x ≤ n • y
.
Main definitions #
archimedean
is a typeclass for an ordered additive commutative monoid to have the archimedean property.archimedean.floor_ring
defines a floor function on an archimedean linearly ordered ring making it into afloor_ring
.
Main statements #
ℕ
,ℤ
, andℚ
are 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
.
An archimedean decidable linearly ordered add_comm_group
has a version of the floor: for
a > 0
, any g
in the group lies between some two consecutive multiples of a
.
Every positive x
is between two successive integer powers of
another y
greater than one. This is the same as exists_mem_Ioc_zpow
,
but with ≤ and < the other way around.
Every positive x
is between two successive integer powers of
another y
greater than one. This is the same as exists_mem_Ico_zpow
,
but with ≤ and < the other way around.
For any y < 1
and any positive x
, there exists n : ℕ
with y ^ n < x
.
Given x
and y
between 0
and 1
, x
is between two successive powers of y
.
This is the same as exists_nat_pow_near
, but for elements between 0
and 1
A linear ordered archimedean ring is a floor ring. This is not an instance
because in some
cases we have a computable floor
function.
Equations
- archimedean.floor_ring α = floor_ring.of_floor α (λ (a : α), classical.some _) _
A linear ordered field that is a floor ring is archimedean.