mathlib

591992d7 - chore(data/real/basic,number_theory/padics/padic_numbers): eliminate `real.of_rat` and `padic.of_rat` (#15569)

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 ```lean #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.