instAlgebraLocalizationAtPrime — Mathlib

English

There is a canonical IsScalarTower for Localization.AtPrime p as a tower over Localization M, showing compatibility of scalar actions via prime localization.

Русский

Существует каноническая скалярная башня для Localization.AtPrime p над Localization M, обеспечивающая совместимость действий скаляров через локализацию по простому.

LaTeX

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

Lean4

noncomputable instance instAlgebraLocalizationAtPrime (x : Ideal R) [H : x.IsPrime] [IsDomain R] :
    Algebra (Localization.AtPrime x) (Localization (nonZeroDivisors R)) :=
  localizationAlgebraOfSubmonoidLe _ _ x.primeCompl (nonZeroDivisors R)
    (by
      intro a ha
      rw [mem_nonZeroDivisors_iff_ne_zero]
      exact fun h => ha (h.symm ▸ x.zero_mem))

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