Commit 2024-06-24 15:56 7ce2b09f

View on Github →

feat(Data/Int/Defs): Basic divisibility lemmas (#13934) Those lemmas already exist for Nat. Also rename Nat.dvd_div_iff to Nat.dvd_div_iff_mul_dvd. From LeanCamCombi

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/Data/Int/Defs.lean

added theorem Int.div_dvd_iff_dvd_mul

added theorem Int.dvd_div_iff_mul_dvd

added theorem Int.dvd_div_of_mul_dvd

added theorem Int.dvd_mul_of_div_dvd

added theorem Int.mul_dvd_of_dvd_div

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

deleted theorem Int.dvd_div_of_mul_dvd

Modified Mathlib/Data/Nat/Defs.lean

deleted theorem Nat.dvd_div_iff

added theorem Nat.dvd_div_iff_mul_dvd

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/GCD/Basic.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean