Commit 2022-07-21 16:19 591992d7View on Github →
padic.of_rat in favor of using
rat.cast directly now that the diamond is gone.
The cauchy version is still useful because it generalizes to fields other than the rationals.
This also cleans up the lemmas around these definitions.
As a bonus, this means the cast from rat to real is now computable, such that
#eval ((2.5 : ℚ) : ℝ).cauchy.unquot 0 -- 5/2
can be used to extract an element of the cauchy series.
It's not clear to me why the
field Cauchy was only a
def and not an
instance. On the assumption that if there were a good reason it would either be indicated in a comment or by a CI failure, I've changed it to be an instance.
This also makes some instances on
padic computable, simply by not defining them in terms of forgetting division from the noncompuable field structure.