Commit 2026-03-17 12:17 c271878a

View on Github →

feat(DedekindDomain/Factorization): add iInf version of finprod_heightOneSpectrum_factorization (#35539) This PR adds an iInf version of finprod_heightOneSpectrum_factorization. This requires two lemmas:

prod_eq_iInf_of_coprime - An iInf version of mul_eq_inf_of_coprime.
HeightOneSpectrum.pow_sup_pow_eq_top - Bundled up version of Ideal.IsMaximal.coprime_of_ne + Ideal.pow_sup_pow_eq_top for HeightOneSpectrum.

Estimated changes

Modified Mathlib/Algebra/Module/DedekindDomain.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

added theorem Ideal.iInf_maxPowDividing_eq

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

added theorem IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod

added theorem IsDedekindDomain.HeightOneSpectrum.isCoprime_of_ne

added theorem IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne

added def IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEq

added theorem IsDedekindDomain.inf_pow_eq_prod_of_prime

deleted theorem IsDedekindDomain.inf_prime_pow_eq_prod

added def IsDedekindDomain.quotientEquivPiFactors

added def IsDedekindDomain.quotientEquivPiOfFinsetProdEq

added def IsDedekindDomain.quotientEquivPiOfProdEq

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.mul_eq_inf_of_isCoprime

added theorem Ideal.prod_eq_iInf_of_pairwise_isCoprime

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean