English
IsDedekindDomainInv A implies A is integrally closed.
Русский
IsDedekindDomainInv A влечет за собой, что A интегрально замкнут.
LaTeX
$$$$\\text{IsDedekindDomainInv}(A) \\Rightarrow \\text{IsIntegrallyClosed}(A).$$$$
Lean4
theorem integrallyClosed : IsIntegrallyClosed A := by
-- It suffices to show that for integral `x`,
-- `A[x]` (which is a fractional ideal) is in fact equal to `A`.
refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)
rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot, Submodule.one_eq_span,
← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (h.isUnit _)]
· exact mem_adjoinIntegral_self A⁰ x hx
· exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A { x }).one_mem)
