# Commit 2024-05-13 15:49 de055554

View on Github →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.