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
.