Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

added theorem real.cauchy_int_cast
added theorem real.cauchy_nat_cast
added theorem real.cauchy_rat_cast
deleted def real.of_rat
deleted theorem real.of_rat_apply
deleted theorem real.of_rat_eq_cast
deleted theorem real.of_rat_lt
added theorem real.rat_cast_lt
deleted theorem padic.cast_eq_of_rat
modified theorem padic.coe_add
modified theorem padic.coe_div
modified theorem padic.coe_mul
modified theorem padic.coe_neg
modified theorem padic.coe_one
modified theorem padic.coe_sub
deleted def padic.of_rat
deleted theorem padic.of_rat_add
deleted theorem padic.of_rat_div
deleted theorem padic.of_rat_eq
deleted theorem padic.of_rat_mul
deleted theorem padic.of_rat_neg
deleted theorem padic.of_rat_one
deleted theorem padic.of_rat_sub
deleted theorem padic.of_rat_zero
modified theorem padic_norm_e.eq_padic_norm'