Commit 2022-12-14 08:34 9a73893b

View on Github →

feat: Port Data.Int.Order.Lemmas (#1002) Based off mathlib3 SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

Created Mathlib/Data/Int/Order/Lemmas.lean

added theorem Int.dvd_div_of_mul_dvd

added theorem Int.eq_zero_of_abs_lt_dvd

added theorem Int.natAbs_eq_iff_mul_self_eq

added theorem Int.natAbs_le_iff_mul_self_le

added theorem Int.natAbs_lt_iff_mul_self_lt