Commit 2022-07-02 12:02 4823da23

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.