dvd_cancel_left_mem_nonZeroDivisors

English

If r is a non-zero-divisor in a ring R, then for all x,y in R, rx divides ry if and only if x divides y.

Русский

Если r является неабсолютно не делителем нуля в кольце R, то для любых x,y ∈ R выполняется, что rx делится ry тогда и только тогда, когда x делит y.

LaTeX

$$$r \in \operatorname{NZD}(R) \Rightarrow (rx \mid ry \iff x \mid y)$$$

Lean4

theorem dvd_cancel_left_mem_nonZeroDivisors (hr : r ∈ R⁰) : r * x ∣ r * y ↔ x ∣ y :=
  (isLeftRegular_iff_mem_nonZeroDivisorsLeft.mpr hr.1).dvd_cancel_left

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