English
IsDedekindDomainInv A holds for a domain A if and only if IsDedekindDomain A holds.
Русский
IsDedekindDomainInv A справедливо тогда и только тогда, когда IsDedekindDomain A справедлив.
LaTeX
$$$$\\text{IsDedekindDomainInv}(A) \\iff \\text{IsDedekindDomain}(A).$$$$
Lean4
theorem mul_inv_cancel_of_le_one [h : IsDedekindDomain A] {I : Ideal A} (hI0 : I ≠ ⊥)
(hI : (I * (I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤ 1) : I * (I : FractionalIdeal A⁰ K)⁻¹ = 1 := by
-- We'll show a contradiction with `exists_notMem_one_of_ne_bot`:
-- `J⁻¹ = (I * I⁻¹)⁻¹` cannot have an element `x ∉ 1`, so it must equal `1`.
obtain ⟨J, hJ⟩ : ∃ J : Ideal A, (J : FractionalIdeal A⁰ K) = I * (I : FractionalIdeal A⁰ K)⁻¹ :=
le_one_iff_exists_coeIdeal.mp mul_one_div_le_one
by_cases hJ0 : J = ⊥
· subst hJ0
refine absurd ?_ hI0
rw [eq_bot_iff, ← coeIdeal_le_coeIdeal K, hJ]
exact coe_ideal_le_self_mul_inv K I
by_cases hJ1 : J = ⊤
· rw [← hJ, hJ1, coeIdeal_top]
exact (not_inv_le_one_of_ne_bot (K := K) hJ0 hJ1 (hJ ▸ hI)).elim
