to_map_eq_zero_iff — Mathlib

English

If M ⊆ nonZeroDivisors(R), then the localization map algebraMap R S is injective. More precisely, under the hypothesis that every element of M is regular, the map algebraMap R S is injective.

Русский

Если M ⊆ nonZeroDivisors(R), то алгебраическая карта из R в S инъективна. Более конкретно, при условии, что каждый элемент M является регулярным, отображение algebraMap R S инъективно.

LaTeX

$$$(\\forall m:\\, m \\in M, \\text{IsRegular}(m)) \\implies \\text{Injective}(\\mathrm{algebraMap}\\ R S)$$$

Lean4

theorem to_map_eq_zero_iff {x : R} (hM : M ≤ nonZeroDivisors R) : algebraMap R S x = 0 ↔ x = 0 :=
  by
  constructor <;> intro h
  · obtain ⟨c, hc⟩ := (map_eq_zero_iff M _ _).mp h
    exact (hM c.2).1 x hc
  · rw [h, map_zero]

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