Commit 2023-06-06 10:51 9f0fbd0c

View on Github →

feat: port RingTheory.DedekindDomain.Factorization (#4721)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/Factorization.lean

added theorem Associates.finite_factors

added theorem Associates.finprod_ne_zero

added theorem Ideal.finite_factors

added theorem Ideal.finite_mulSupport

added theorem Ideal.finite_mulSupport_coe

added theorem Ideal.finite_mulSupport_inv

added theorem Ideal.finprod_count

added theorem Ideal.finprod_heightOneSpectrum_factorization

added theorem Ideal.finprod_heightOneSpectrum_factorization_coe

added theorem Ideal.finprod_not_dvd

added def IsDedekindDomain.HeightOneSpectrum.maxPowDividing