isLocalization_of_isSeparable — Mathlib

English

If L is algebraic over K and L has no zero-divisors with respect to A, then L is separable over the fraction ring after AtPrime localization.

Русский

Если L над K является алгебраическим, и L не имеет нулевых делителей по отношению к A, то после локализации AtPrime дробные кольца образуют сепарабельное расширение.

LaTeX

$$$\text Algebra.IsSeparable (FractionRing AtPrime) (FractionRing (Localization AtPrime))$$$

Lean4

theorem isLocalization_of_isSeparable [IsDomain A] [Algebra.IsSeparable K L] :
    IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L :=
  IsIntegralClosure.isLocalization A K L C

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