Commit 2025-07-31 15:44 f5dca229

View on Github →

chore: split long file DedekindDomain/Ideal.lean (#27676) This PR splits Mathlib/RingTheory/DedekindDomain/Ideal.lean into three parts:

  • FractionalIdeal/Inverse.lean defines the Inv operator on fractional ideals, and proves basic results.
  • DedekindDomain/Ideal/Basic.lean defines IsDedekindDomainInv, shows equivalence with IsDedekindDomain and provides unique factorization instances. This is sufficient for ClassGroup.lean.
  • DedekindDomain/Ideal/Lemmas.lean defines HeightOneSpectrum and contains remaining lemmas. Also upstream a lemma that doesn't refer to Dedekind domains.

Estimated changes

added theorem Ideal.dvd_iff_le
added theorem one_mem_inv_coe_ideal
deleted theorem FractionalIdeal.inv_eq
deleted theorem FractionalIdeal.inv_zero'
deleted theorem Ideal.dvdNotUnit_iff_lt
deleted theorem Ideal.dvd_iff_le
deleted def IsDedekindDomainInv
deleted theorem isDedekindDomainInv_iff
deleted theorem one_mem_inv_coe_ideal
added theorem FractionalIdeal.inv_eq