Commit 2024-04-15 14:21 28bea03d

View on Github →

refactor(Rat): Streamline basic theory (#11504) Rat has a long history in (and before) mathlib and as such its development is full of cruft. Now that NNRat is a thing, there is a need for the theory of Rat to be mimickable to yield the theory of NNRat, which is not currently the case. Broadly, this PR aims at mirroring the Rat and NNRat declarations. It achieves this by:

  • Relying more on Rat.num and Rat.den, and less on the structure representation of Rat
  • Abandoning the vestigial Rat.Nonneg (which was replaced in Std by a new development of the order on Rat)
  • Renaming many Rat lemmas with dubious names. This creates quite a lot of conflicts with Std lemmas, whose names are themselves dubious. I am priming the relevant new mathlib names and leaving TODOs to fix the Std names.
  • Handling most of the Rat porting notes Reduce the diff of #11203

Estimated changes

added theorem NNRat.add_def
added theorem NNRat.coe_divNat
added theorem NNRat.coprime_num_den
deleted def NNRat.den
modified theorem NNRat.den_coe
added theorem NNRat.den_ne_zero
added def NNRat.divNat
added theorem NNRat.divNat_inj
added theorem NNRat.mk_divInt
added theorem NNRat.mul_def
deleted def NNRat.num
added theorem NNRat.num_divNat_den
deleted def NNRat
deleted theorem NNRat.coe_div
deleted theorem NNRat.coe_inv
modified theorem Rat.cast_add_of_ne_zero
modified theorem Rat.cast_div_of_ne_zero
deleted theorem Rat.cast_eq_id
deleted theorem Rat.cast_id
modified theorem Rat.cast_inv_of_ne_zero
deleted theorem Rat.cast_mk_of_ne_zero
modified theorem Rat.cast_mul_of_ne_zero
modified theorem Rat.cast_neg
modified theorem Rat.cast_sub_of_ne_zero
modified theorem eq_ratCast
added theorem Rat.divInt_div_divInt
modified theorem Rat.divInt_eq_div
added theorem Rat.divInt_mul_divInt'
added theorem Rat.divInt_neg
deleted theorem Rat.divInt_neg_den
modified theorem Rat.divInt_neg_one_one
modified theorem Rat.divInt_one
modified theorem Rat.divInt_one_one
added theorem Rat.divInt_self'
modified theorem Rat.divInt_zero_one
added theorem Rat.div_def'
deleted theorem Rat.div_num_den
modified theorem Rat.intCast_eq_divInt
modified theorem Rat.inv_def'
added theorem Rat.inv_divInt'
added theorem Rat.inv_mkRat
added theorem Rat.mk'_eq_divInt
modified theorem Rat.mkRat_eq_div
modified theorem Rat.mkRat_one
modified theorem Rat.mul_def'
deleted theorem Rat.mul_num_den
modified theorem Rat.neg_def
deleted theorem Rat.num_den'
deleted theorem Rat.num_den
added theorem Rat.num_divInt_den
modified theorem Rat.sub_def''
modified theorem Rat.zero_of_num_zero
added theorem NNRat.coe_div
added theorem NNRat.coe_inv
added theorem NNRat.div_def
added theorem NNRat.inv_def
added def NNRat.den
added theorem NNRat.den_mk
added def NNRat.num
added theorem NNRat.num_mk
added def NNRat
added theorem Rat.cast_eq_id
added theorem Rat.cast_id
deleted theorem Rat.inv_def''
modified theorem Rat.divInt_nonneg
added theorem Rat.mkRat_nonneg
deleted theorem Rat.nonneg_iff_zero_le
modified theorem Rat.num_nonneg
modified theorem Rat.sqrt_nonneg