localization_comap_injective — Mathlib

English

Let M be a submonoid and S a localization; the map comap (algebraMap R S) is injective.

Русский

Пусть M — подмножество и S — локализация; отображение comap (algebraMap R S) инъективно.

LaTeX

$$Function.Injective (comap (algebraMap R S)).$$

Lean4

theorem localization_comap_injective [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    Function.Injective (comap (algebraMap R S)) := fun _ _ h => localization_specComap_injective S M h

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