mk'_eq_zero_iff — Mathlib

English

For any x ∈ R and s ∈ M, the fraction x/s is equal to zero in the localization S if and only if there exists m ∈ M with m·x = 0 in R.

Русский

Для любых x ∈ R и s ∈ M дробь x/s равна нулю в локализации S тогда и только тогда, когда существует m ∈ M такое, что m·x = 0 в R.

LaTeX

$$$\\dfrac{x}{s} = 0 \\iff \\exists m \\in M,\\; m x = 0.$$$

Lean4

theorem mk'_eq_zero_iff (x : R) (s : M) : mk' S x s = 0 ↔ ∃ m : M, ↑m * x = 0 :=
  (toLocalizationMap M S).mk'_eq_zero_iff x s

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