mathlib3

12d63a7f - feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime (#17877)

feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime (#17877) We add `exists_eq_pow_of_mul_eq_pow_of_coprime`: this is done for semirings, in order to apply to `ideal R` for a Dedekind domain `R`. Corresponding mathlib4 PR [#928](https://github.com/leanprover-community/mathlib4/pull/928).