mathlib3

ae0d10f6 - feat(ring_theory/dedekind_domain/factorization): add factorization lemmas (#17915)

feat(ring_theory/dedekind_domain/factorization): add factorization lemmas (#17915) This is the first in a sequence of PRs to prove that every nonzero fractional ideal of a Dedekind domain `R` can be factored as a finprod `∏_v v^{n_v}` over the maximal ideals of `R`, where the exponents `n_v` are integers, and to provide related API. In this PR we prove the analogous statement for ideals of `R`.