ne_zero_of_mk'_ne_zero — Mathlib

English

If R has no zero divisors, then any localization S of R at M also has no zero divisors.

Русский

Если у R нет нулевых делителей, то и локализация S локализации R по M также не имеет нулевых делителей.

LaTeX

$$$[NoZeroDivisors \\, R] \\Rightarrow [NoZeroDivisors \\, S],$$$

Lean4

theorem ne_zero_of_mk'_ne_zero {x : R} {y : M} (hxy : IsLocalization.mk' S x y ≠ 0) : x ≠ 0 :=
  by
  rintro rfl
  exact hxy (IsLocalization.mk'_zero _)

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