Commit 2022-07-21 16:19 591992d7
View on Github →chore(data/real/basic,number_theory/padics/padic_numbers): eliminate real.of_rat
and padic.of_rat
(#15569)
This removes real.of_rat
and 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 Cauchy
and padic
computable, simply by not defining them in terms of forgetting division from the noncompuable field structure.