instAlgebraLocalizationAlgebraMapSubmonoid

English

There is a natural Algebra structure on Localization M to Localization (Algebra.algebraMapSubmonoid S M).

Русский

Существует естественная структура алгебры на Localization M к Localization (Algebra.algebraMapSubmonoid S M).

LaTeX

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

Lean4

noncomputable instance : Algebra (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)) :=
  localizationAlgebra M S

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