Commit 2023-01-01 21:48 3382f76a

View on Github →

feat: port Data.Int.ModEq (#1285)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/ModEq.lean

added theorem Dvd.dvd.modEq_zero_int

added theorem Dvd.dvd.zero_modEq_int

added theorem Int.ModEq.dvd

added theorem Int.ModEq.of_modEq_mul_left

added theorem Int.ModEq.of_modEq_mul_right

added def Int.ModEq

added theorem Int.coe_nat_modEq_iff

added theorem Int.exists_unique_equiv

added theorem Int.exists_unique_equiv_nat

added theorem Int.gcd_a_modEq

added theorem Int.modEq_add_fac

added theorem Int.modEq_add_fac_self

added theorem Int.modEq_and_modEq_iff_modEq_mul

added theorem Int.modEq_iff_add_fac

added theorem Int.modEq_iff_dvd

added theorem Int.modEq_of_dvd

added theorem Int.modEq_one

added theorem Int.modEq_sub

added theorem Int.modEq_zero_iff_dvd

added theorem Int.mod_coprime

added theorem Int.mod_modEq

added theorem Int.mod_mul_left_mod

added theorem Int.mod_mul_right_mod