Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-05 16:16 c0dbeca1

View on Github →

chore(data/{int,nat}/modeq): Rationalise lemma names (#17902) Quite a few modeq lemmas are still 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. Also add nat.modeq.eq_of_lt_of_lt as a corollary to nat.modeq.eq_of_abs_lt.

Estimated changes

deleted theorem int.modeq.dvd
added theorem int.modeq.of_mul_left
added theorem int.modeq.of_mul_right
deleted theorem int.modeq_of_dvd
modified theorem nat.add_modeq_left
modified theorem nat.add_modeq_right
added theorem nat.modeq.dvd_iff
added theorem nat.modeq.eq_of_abs_lt
added theorem nat.modeq.gcd_eq
deleted theorem nat.modeq.gcd_eq_of_modeq
added theorem nat.modeq.of_mul_left
added theorem nat.modeq.of_mul_right
deleted theorem nat.modeq_of_dvd
modified theorem nat.modeq_one
modified theorem nat.modeq_sub
modified theorem nat.modeq_zero_iff