Commit 2022-12-14 08:49 3bcd786d

View on Github →

feat : port Data.Int.Dvd.Basic (#996) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e Easy.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Dvd/Basic.lean

added theorem Int.coe_nat_dvd

added theorem Int.coe_nat_dvd_left

added theorem Int.coe_nat_dvd_right

added theorem Int.dvd_natAbs_of_ofNat_dvd

added theorem Int.ofNat_dvd_of_dvd_natAbs