injectiveₛ — Mathlib

English

For IsLocalization, if hM: M ≤ nonZeroDivisors(R), then the localization algebra map algebraMap R S is injective.

Русский

Для локализации, если hM: M ⊆ nonZeroDivisors(R), то отображение algebraMap R S инъективно.

LaTeX

$$$(M \\leq \\text{nonZeroDivisors}(R)) \\Rightarrow \\text{Injective}(\\mathrm{algebraMap}\\ R S)$$$

Lean4

protected theorem injectiveₛ (hM : ∀ m ∈ M, IsRegular m) : Injective (algebraMap R S) :=
  (toLocalizationMap M S).injective_iff.mpr hM

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