Commit 2024-04-06 09:41 9160ea19

View on Github →

refactor: Avoid Rat internals in the definition of Field (#11639) Soon, there will be NNRat analogs of the Rat fields in the definition of Field. NNRat is less nicely a structure than Rat, hence there is a need to reduce the dependency of Field on the internals of Rat. This PR achieves this by restating Field.ratCast_mk' in terms of Rat.num, Rat.den. This requires fixing a few downstream instances. Reduce the diff of #11203.

Estimated changes

modified def Rat.castRec
modified theorem Rat.cast_def
modified theorem Rat.cast_mk'
modified theorem Rat.smul_def
modified theorem CauSeq.Completion.ofRat_div
modified theorem Quaternion.coe_rat_cast
modified theorem Quaternion.rat_cast_im
modified theorem Quaternion.rat_cast_imI
modified theorem Quaternion.rat_cast_imJ
modified theorem Quaternion.rat_cast_imK
modified theorem Quaternion.rat_cast_re
modified theorem Complex.div_im
modified theorem Complex.div_re
modified theorem Complex.im_ofNat
modified theorem Complex.int_cast_im
modified theorem Complex.int_cast_re
modified theorem Complex.nat_cast_im
modified theorem Complex.nat_cast_re
modified theorem Complex.ofReal_int_cast
modified theorem Complex.ofReal_nat_cast
modified theorem Complex.ofReal_ofNat
added theorem Complex.ofReal_qsmul
modified theorem Complex.ofReal_rat_cast
modified theorem Complex.rat_cast_im
modified theorem Complex.rat_cast_re
modified theorem Complex.re_ofNat
added theorem Rat.den_ne_zero
modified theorem Real.cauchy_intCast
modified theorem Real.cauchy_natCast
modified theorem Real.cauchy_ratCast
added theorem Real.ofCauchy_div
modified theorem Real.ofCauchy_intCast
modified theorem Real.ofCauchy_natCast
modified theorem Real.ofCauchy_ratCast