Commit 2022-03-03 14:50 8053f56d
View on Github →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.