mathlib3
c765b044 - chore(data/(int, nat)/modeq): rationalize lemma names (#8644)

Commit
4 years ago
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
Author
Parents
Loading