Commit 2024-02-12 10:30 2357b645

View on Github →

chore(NNRat): Rearrange imports (#10392) The goal is to separate the field material on Rat/NNRat from everything before to make way for NNRat.cast. We achieve this by

  • splitting Data.Rat.NNRat into
    • Data.NNRat.Defs for the foundationl stuff that will be needed in the definition of Field
    • Data.NNRat.Lemmas for the field and big operators material
  • moving the field material from Data.Rat.Order to Data.Rat.Basic
  • proving a few lemmas by rfl rather than coeHom.some_now_unavailable_lemma
  • renaming Data.Rat.NNRat.BigOperators to Data.NNRat.BigOperators

Estimated changes

deleted theorem NNRat.coe_div
deleted theorem NNRat.coe_indicator
deleted theorem NNRat.coe_inv
deleted theorem NNRat.num_div_den
deleted theorem Rat.toNNRat_div'
deleted theorem Rat.toNNRat_div
deleted theorem Rat.toNNRat_inv
added theorem NNRat.coe_div
added theorem NNRat.coe_indicator
added theorem NNRat.coe_inv
added theorem NNRat.num_div_den
added theorem Rat.toNNRat_div'
added theorem Rat.toNNRat_div
added theorem Rat.toNNRat_inv