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.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Author: 3 people