mathlib3

20c144b5 - feat(ring_theory/dedekind_domain): lemmas on inequality between ideal powers (#17188)

feat(ring_theory/dedekind_domain): lemmas on inequality between ideal powers (#17188) We prove some basic results on sublists, for corollaries on multisets, for corollaries for sets of factors, so that we can prove that successive powers of a prime ideal in a Dedekind domain are predecessors. This is useful for showing that the ideal norm is multiplicative for prime powers in a Dedekind domain.