instFiniteDimensionalFractionRingOfFinite

English

If L is a finite separable extension and A is integrally closed, then the localized integral closure is principal after appropriate localization of coefficients.

Русский

Если L — конечное сепарабельноe расширение и A интегрально замкнуто, то локализация интегрального замыкания становится главной (principal).

LaTeX

$$$$\\text{loc-principal}(\\text{integralClosure } A L)$$$$

Lean4

instance [Module.Finite A C] [NoZeroSMulDivisors A C] : FiniteDimensional (FractionRing A) (FractionRing C) :=
  .of_isLocalization A C A⁰

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