instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors

English

There exists a finite instance relating FractionRing localization with localization over submonoids.

Русский

Существует конечный экземпляр, устанавливающий связь между FractionRing и локализацией против подмножества.

LaTeX

$$$\\operatorname{instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors}$$$

Lean4

instance {A C : Type*} [CommRing A] [CommRing C] [Algebra A C] [Module.Finite A C] :
    Module.Finite (FractionRing A) (Localization (algebraMapSubmonoid C A⁰)) :=
  have : IsScalarTower A (FractionRing A) (Localization (algebraMapSubmonoid C A⁰)) :=
    instIsScalarTowerLocalizationAlgebraMapSubmonoid A⁰ C
  .of_isLocalization A C A⁰

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