Commit 2024-04-24 05:40 7e72dffd

View on Github →

chore: unify date formatting in lemma deprecations (#12334)

  • consistently use the YYYY-MM-DD format
  • when easily possible, put the date on the same line as the deprecated attribute
  • when easily possible, format the entire declaration on the same line Why these changes?
  • consistency makes it easier for tools to parse this information
  • compactness: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway
  • putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968

Estimated changes

modified theorem two_smul'
modified theorem Complex.int_cast_abs
modified theorem Rat.divInt_neg_one_one
modified theorem Rat.divInt_zero_one
modified theorem Rat.sub_def''