isIntegral_of_mem_ringOfIntegers — Mathlib

English

Every element of the integral closure of the valuation subring in L is integral over the valuation subring itself.

Русский

Каждый элемент интегрального замыкания надценного подкольца в L является интегралом над самим подкольцом оценки.

LaTeX

$$$\\forall x \\in \\mathrm{integralClosure}(v.valuationSubring L),\\; x\\text{ is integral over } v.valuationSubring.$$$

Lean4

theorem isIntegral_of_mem_ringOfIntegers {x : L} (hx : x ∈ integralClosure v.valuationSubring L) :
    IsIntegral v.valuationSubring (⟨x, hx⟩ : integralClosure v.valuationSubring L) :=
  integralClosure.isIntegral ⟨x, hx⟩

Похожие утверждения