Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-03 08:03 402f8982

View on Github →

chore(algebra/order/group/basic): Improve lemma names (#16970) Rename

  • div_le'' → div_le_comm
  • le_div'' → le_div_comm
  • sub_le → sub_le_comm
  • le_sub → le_sub_comm
  • div_lt'' → div_lt_comm
  • lt_div'' → lt_div_comm
  • sub_lt → sub_lt_comm
  • lt_sub → lt_sub_comm

Estimated changes

modified theorem int.fract_lt_one
deleted theorem div_le''
added theorem div_le_comm
deleted theorem div_lt''
added theorem div_lt_comm
deleted theorem le_div''
added theorem le_div_comm
deleted theorem lt_div''
added theorem lt_div_comm