English
Let A be an integral domain with a field K and assume A is a Dedekind domain in the inverse sense. Then every nonzero fractional ideal I of A has a two-sided inverse I^{-1} and satisfies I · I^{-1} = 1.
Русский
Пусть A — целое домино, поле K содержит A как полную дробную сферу; пусть A является Дединдовым доменом в смысле обратимости. Тогда любой не нулевой дробный идеал I имеет обратный I^{-1}, и выполняется I · I^{-1} = 1.
LaTeX
$$$$\\IsDedekindDomainInv(A) \\;\Longleftrightarrow\\; \\forall I\\,(I \\neq 0)\\;:\\; I \\cdot I^{-1} = 1.$$$$
Lean4
theorem isDedekindDomainInv_iff [Algebra A K] [IsFractionRing A K] :
IsDedekindDomainInv A ↔ ∀ I ≠ (⊥ : FractionalIdeal A⁰ K), I * I⁻¹ = 1 :=
by
let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K :=
FractionalIdeal.mapEquiv (FractionRing.algEquiv A K)
refine h.toEquiv.forall_congr (fun {x} => ?_)
rw [← h.toEquiv.apply_eq_iff_eq]
simp [h]
