Commit 2024-04-24 20:27 a93cf157

View on Github →

feat(Nat/GCD): Add dvd_gcd_mul_gcd_of_dvd_mul (#12246)

Estimated changes

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

added theorem Nat.dvd_gcd_mul_gcd_iff_dvd_mul

added theorem Nat.dvd_gcd_mul_iff_dvd_mul

added theorem Nat.dvd_mul_gcd_iff_dvd_mul

added theorem Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime