instIsScalarTowerLocalizationAlgebraMapSubmonoid

English

There is a scalar tower IsScalarTower R (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)).

Русский

Существует торовая структура скаляров IsScalarTower между R, Localization M и Localization (Algebra.algebraMapSubmonoid S M).

LaTeX

$$$\text{IsScalarTower}(R, (\text{Localization } M), (\text{Localization } (\text{Algebra.algebraMapSubmonoid } S M)))$$$

Lean4

instance : IsScalarTower R (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)) :=
  IsScalarTower.of_algebraMap_eq
    (fun x ↦ (IsLocalization.map_eq (T := (Algebra.algebraMapSubmonoid S M)) M.le_comap_map x).symm)

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