instIsScalarTowerAtPrimeFractionRing_1

English

Assuming NoZeroDivisors and faithful SMul, the separability transfers to fraction rings after AtPrime localization.

Русский

При отсутствии нулевых делителей и верной скалярной операции разделимость переносится на дробные кольца после локализации AtPrime.

LaTeX

$$$\text{Algebra.IsSeparable} (\FractionRing (Localization.AtPrime P)) (\FractionRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)))$$$

Lean4

instance : IsScalarTower R Rₚ K :=
  of_algebraMap_eq' (RingHom.ext fun x ↦ by simp [RingHom.algebraMap_toAlgebra])

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