Cauchy completion #
This file generalizes the Cauchy completion of
(ℚ, abs) to the completion of a ring
with absolute value.
The map from the original ring into the Cauchy completion.
The Cauchy completion forms a division ring.
Show the first 10 items of a representative of this equivalence class of cauchy sequences.
The representative chosen is the one passed in the VM to
Quot.mk, so two cauchy sequences
converging to the same number may be printed differently.
- One or more equations did not get rendered due to their size.
A class stating that a ring with an absolute value is complete, i.e. every Cauchy sequence has a limit.
Every Cauchy sequence has a limit.
The limit of a Cauchy sequence in a complete ring. Chosen non-computably.