Commit 2021-08-14 06:36 c765b044

chore(data/(int, nat)/modeq): rationalize lemma names (#8644) Many modeq lemmas were called nat.modeq.modeq_something or int.modeq.modeq_something. I'm deleting the duplicated modeq, so that lemmas (usually) become nat.modeq.something and int.modeq.something. Most of them must be protected. This facilitates greatly the use of dot notation on nat.modeq and int.modeq while shortening lemma names. I'm adding a few lemmas:

• nat.modeq.rfl, int.modeq.rfl
• nat.modeq.dvd, int.modeq.dvd
• nat.modeq_of_dvd, int.modeq_of_dvd
• has_dvd.dvd.modeq_zero_nat, has_dvd.dvd.zero_modeq_nat, has_dvd.dvd.modeq_zero_int, has_dvd.dvd.zero_modeq_int
• nat.modeq.add_left, nat.modeq.add_right, int.modeq.add_left, int.modeq.add_right
• nat.modeq.add_left_cancel', nat.modeq.add_right_cancel', int.modeq.add_left_cancel', int.modeq.add_right_cancel'
• int.modeq.sub_left, int.modeq.sub_right
• nat.modeq_sub, int.modeq_sub
• int.modeq_one
• int.modeq_pow I'm also renaming some lemmas (on top of the general renaming):
• add_cancel_left -> add_left_cancel, add_cancel_right -> add_right_cancel
• modeq_zero_iff -> modeq_zero_iff_dvd in prevision of an upcoming PR