Cauchy completion #
This file generalizes the Cauchy completion of (ℚ, abs)
to the completion of a ring
with absolute value.
The Cauchy completion of a ring with absolute value.
Equations
Instances For
The map from Cauchy sequences into the Cauchy completion.
Equations
Instances For
The map from the original ring into the Cauchy completion.
Equations
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
CauSeq.Completion.ofRat
as a RingHom
Equations
Instances For
Equations
Equations
Equations
Equations
Equations
The Cauchy completion forms a division ring.
Equations
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.
Equations
The Cauchy completion forms a field.
Equations
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.
Instances
The limit of a Cauchy sequence in a complete ring. Chosen non-computably.