English
There is an algebra structure on the localization algebra at prime and its prime-complement companion.
Русский
Существует структура алгебры на локализации AtPrime и её локализации по primeCompl.
LaTeX
$$$\IsLocalization\ (Algebra.algebraMapSubmonoid S P.primeCompl)\ (Localization\ (Algebra.algebraMapSubmonoid S P.primeCompl))$$$
Lean4
instance [Algebra.IsSeparable K L] :
-- Without the following line there is a timeout
letI : Algebra Rₚ (FractionRing Sₚ) := OreLocalization.instAlgebra
Algebra.IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) :=
let _ : Algebra Rₚ (FractionRing Sₚ) := OreLocalization.instAlgebra
FractionRing.isSeparable_of_isLocalization S _ _ P.primeCompl_le_nonZeroDivisors
