Commit 2024-05-13 15:49 de055554

feat(RingTheory.DedekindDomain.Factorization): add factorization of fractional ideals (#7778) We show that every nonzero fractional ideal I 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. We define FractionalIdeal.count K v I to be n_v, and we prove some of its properties.