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_lesub_le_comm
  • le_suble_sub_comm
  • div_lt''div_lt_comm
  • lt_div''lt_div_comm
  • sub_ltsub_lt_comm
  • lt_sublt_sub_comm

Estimated changes

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