injective — Mathlib

English

For IsLocalization, if M ≤ nonZeroDivisors(R) then the algebra map algebraMap R S is injective, i.e., the localization map preserves distinctness.

Русский

Для IsLocalization при M ≤ nonZeroDivisors(R) отображение algebraMap R S инъективно, т.е. сохранение различности локализации.

LaTeX

$$$\\text{IsLocalization.injective}\\ (M\\ S)$$$

Lean4

protected theorem injective (hM : M ≤ nonZeroDivisors R) : Injective (algebraMap R S) :=
  IsLocalization.injectiveₛ S fun _x hx ↦ isRegular_iff_mem_nonZeroDivisors.mpr (hM hx)

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