dvd_cancel_left_coe_nonZeroDivisors

English

If r is a non-zero-divisor in a ring R, then for all x,y in R, rx divides ry iff 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_coe_nonZeroDivisors {c : R⁰} : c * x ∣ c * y ↔ x ∣ y :=
  dvd_cancel_left_mem_nonZeroDivisors c.prop

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