isIntegral_of_mem_ringOfIntegers'

English

If x belongs to the integral closure of the valuation subring, then x considered as an element of the closure is integral over the subring.

Русский

Если x принадлежит интегральному замыканию подкольца оценки, то x в замыкании является интегралом над подкольцом.

LaTeX

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

Lean4

theorem isIntegral_of_mem_ringOfIntegers' {x : (integralClosure v.valuationSubring L)} :
    IsIntegral v.valuationSubring (x : integralClosure v.valuationSubring L) := by
  apply isIntegral_of_mem_ringOfIntegers

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