instIsScalarTowerAtPrimeFractionRing

English

There is a scalar tower R → Localization.AtPrime p → FractionRing R, giving a chain from R to its fraction ring through the prime localization.

Русский

Через простую локализацию p строится цепь к FractionRing R.

LaTeX

$$IsScalarTower R (Localization.AtPrime p) (FractionRing R)$$

Lean4

instance {R : Type*} [CommRing R] [IsDomain R] (p : Ideal R) [p.IsPrime] :
    IsScalarTower R (Localization.AtPrime p) (FractionRing R) :=
  localization_isScalarTower_of_submonoid_le (Localization.AtPrime p) (FractionRing R) p.primeCompl (nonZeroDivisors R)
    p.primeCompl_le_nonZeroDivisors

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