mathlib documentation

topology.algebra.order.archimedean

Rational numbers are dense in a linear ordered archimedean field #

In this file we prove that coercion from to a linear ordered archimedean field has dense range. This lemma is in a separate file because topology.order.basic does not import algebra.order.archimedean.

Rational numbers are dense in a linear ordered archimedean field.