English
If R is an integrally closed ring and K is a field containing R via a fraction construction, then the integral closure of R in K coincides with the smallest subalgebra of K (the bottom element). In particular, every element of the integral closure lies in the base subalgebra.
Русский
Если R является интегрально замкнутым кольцом и K — поле, содержащее R через дробовую конструкцию, то интегральное замыкание R в K совпадает с наименьшей подалгеброй K (нижняя граница). В частности, каждый элемент интегрального замыкания принадлежит базовой подалгебре.
LaTeX
$$$\\operatorname{integralClosure}(R,K)=\\bot$$$
Lean4
/-- This is almost a duplicate of `IsIntegrallyClosedIn.integralClosure_eq_bot`,
except the `NoZeroSMulDivisors` hypothesis isn't inferred automatically from `IsFractionRing`. -/
@[simp]
theorem integralClosure_eq_bot [IsIntegrallyClosed R] : integralClosure R K = ⊥ :=
(integralClosure_eq_bot_iff K).mpr ‹_›
