English
In a Dedekind domain, an ideal I divides another ideal J if and only if J is contained in I.
Русский
В детерминантовом домене делимость идеала I на другой идеал J эквивалентна тому, что J содержится в I.
LaTeX
$$$I \mid J \iff J \le I$$$
Lean4
/-- For ideals in a Dedekind domain, to divide is to contain. -/
theorem dvd_iff_le {I J : Ideal A} : I ∣ J ↔ J ≤ I :=
⟨Ideal.le_of_dvd, fun h => by
by_cases hI : I = ⊥
· have hJ : J = ⊥ := by rwa [hI, ← eq_bot_iff] at h
rw [hI, hJ]
have hI' : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI
have : (I : FractionalIdeal A⁰ (FractionRing A))⁻¹ * J ≤ 1 :=
by
rw [← inv_mul_cancel₀ hI']
exact mul_left_mono _ ((coeIdeal_le_coeIdeal _).mpr h)
obtain ⟨H, hH⟩ := le_one_iff_exists_coeIdeal.mp this
use H
refine coeIdeal_injective (show (J : FractionalIdeal A⁰ (FractionRing A)) = ↑(I * H) from ?_)
rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]⟩
