theorem FractionalIdeal.unique_factorization_exists {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

theorem FractionalIdeal.unique_factorization_unique {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (_hI : I ≠ 0) (e : IsDedekindDomain.HeightOneSpectrum R → ℤ) (he : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, e v = 0) (hprod : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ e v = I) (v : IsDedekindDomain.HeightOneSpectrum R) : e v = count K v I

theorem FractionalIdeal.unique_factorization {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I ∧ ∀ (e : IsDedekindDomain.HeightOneSpectrum R → ℤ), (∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, e v = 0) → ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ e v = I → ∀ (v : IsDedekindDomain.HeightOneSpectrum R), e v = count K v I