instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl

English

There is a scalar tower linking R_p, S_p and T_p after prime-complement localization.

Русский

Существует каскад скалярных торов после локализации по primeCompl, связывающий R_p, S_p и T_p.

LaTeX

$$$\text IsScalarTower (R_p) (S_p) (T_p)$$$

Lean4

instance : IsScalarTower S Sₚ Tₚ :=
  IsScalarTower.of_algebraMap_eq' <| by
    rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

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