Commit 2025-11-12 13:54 07ca3dd5

View on Github →

refactor(FractionalIdeal): use algebraic order theory API (#29538) Instantiate instances earlier and use generic lemmas instead of the FractionalIdeal-specific ones. Also rename _nonzero in lemma names to _ne_zero.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

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

modified theorem FractionalIdeal.coe_ideal_mul_inv

modified theorem FractionalIdeal.mul_inv_cancel_of_le_one

modified theorem FractionalIdeal.mul_left_le_iff

added theorem FractionalIdeal.mul_left_strictMono

modified theorem FractionalIdeal.mul_right_le_iff

modified theorem FractionalIdeal.mul_right_strictMono

modified theorem FractionalIdeal.not_inv_le_one_of_ne_bot

modified theorem IsDedekindDomainInv.dimensionLEOne

deleted theorem IsDedekindDomainInv.inv_mul_eq_one

deleted theorem IsDedekindDomainInv.mul_inv_eq_one

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

deleted theorem FractionalIdeal.mul_left_strictMono

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

added theorem FractionalIdeal.add_le_add_left

modified theorem FractionalIdeal.le_self_mul_self

added theorem FractionalIdeal.mul_le_mul_left

deleted theorem FractionalIdeal.mul_left_mono

deleted theorem FractionalIdeal.mul_right_mono

modified theorem FractionalIdeal.mul_self_le_self

Modified Mathlib/RingTheory/FractionalIdeal/Inverse.lean

added theorem FractionalIdeal.coe_inv_of_ne_zero

deleted theorem FractionalIdeal.coe_inv_of_nonzero

deleted theorem FractionalIdeal.inv_nonzero

added theorem FractionalIdeal.inv_of_ne_zero

modified theorem FractionalIdeal.right_inverse_eq

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

deleted theorem FractionalIdeal.div_nonzero

added theorem FractionalIdeal.div_of_ne_zero

deleted theorem FractionalIdeal.fractional_div_of_nonzero

added theorem FractionalIdeal.isFractional_div_of_ne_zero

added theorem FractionalIdeal.le_div_iff_of_ne_zero

deleted theorem FractionalIdeal.le_div_iff_of_nonzero

added theorem FractionalIdeal.mem_div_iff_of_ne_zero

deleted theorem FractionalIdeal.mem_div_iff_of_nonzero