mathlib

8053f56d - feat(ring_theory/dedekind_domain): strengthen `exist_integer_multiples` (#12184)

feat(ring_theory/dedekind_domain): strengthen `exist_integer_multiples` (#12184) Let `J ≠ ⊤` be an ideal in a Dedekind domain `A`, and `f ≠ 0` a finite collection of elements of `K = Frac(A)`, then we can multiply the elements of `f` by some `a : K` to find a collection of elements of `A` that is not completely contained in `J`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>