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.