Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes