Theorem Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime

Modification history

2024-04-24 20:27
Mathlib/Data/Nat/GCD/Basic.lean
feat(Nat/GCD): Add dvd_gcd_mul_gcd_of_dvd_mul (#12246)
Added Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprimeView on Github →