mathlib

4823da23 - feat(data/nat/basic): add `mul_div_mul_comm_of_dvd_dvd` (#15031)

feat(data/nat/basic): add `mul_div_mul_comm_of_dvd_dvd` (#15031) Add lemma `mul_div_mul_comm_of_dvd_dvd (hac : c ∣ a) (hbd : d ∣ b) : (a * b) / (c * d) = (a / c) * (b / d)` (Compare with `mul_div_mul_comm`, which holds for a `division_comm_monoid`) Also adds the same lemma for a `euclidean_domain`.