English
For nonzero fractional ideals I,J in a Dedekind domain, I ≤ J⁻¹ is equivalent to J ≤ I⁻¹.
Русский
Для непустых дробных идеалов I,J в области Дедекина: I ≤ J^{-1} эквивалентно J ≤ I^{-1}.
LaTeX
$$I ≤ J^{-1} \\iff J ≤ I^{-1}$$
Lean4
/-- Ideals in a Dedekind domain have gcd and lcm operators that (trivially) are compatible with
the normalization operator. -/
noncomputable instance : NormalizedGCDMonoid (Ideal A) :=
{ Ideal.normalizationMonoid with
gcd := (· ⊔ ·)
gcd_dvd_left := fun _ _ => by simpa only [dvd_iff_le] using le_sup_left
gcd_dvd_right := fun _ _ => by simpa only [dvd_iff_le] using le_sup_right
dvd_gcd := by
simp only [dvd_iff_le]
exact fun h1 h2 => @sup_le (Ideal A) _ _ _ _ h1 h2
lcm := (· ⊓ ·)
lcm_zero_left := fun _ => by simp only [zero_eq_bot, bot_inf_eq]
lcm_zero_right := fun _ => by simp only [zero_eq_bot, inf_bot_eq]
gcd_mul_lcm := fun _ _ => by rw [associated_iff_eq, sup_mul_inf]
normalize_gcd := fun _ _ => normalize_eq _
normalize_lcm := fun _ _ => normalize_eq _ }
-- In fact, any lawful gcd and lcm would equal sup and inf respectively.
