Commit 2023-01-18 10:08 9742fc6e

View on Github →

feat: Rationalise ModEq lemma names (#1384) Match https://github.com/leanprover-community/mathlib/pull/17902

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
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_dvd
added theorem Nat.ModEq.of_mul_left
added theorem Nat.ModEq.of_mul_right
modified theorem Nat.add_modEq_left
modified theorem Nat.add_modEq_right
deleted theorem Nat.modEq_of_dvd
modified theorem Nat.modEq_one
modified theorem Nat.modEq_sub
modified theorem Nat.modEq_zero_iff