mul_cancel_right_mem_nonZeroDivisorsRight

English

If r ∈ nonZeroDivisorsRight R, then x r = y r iff x = y.

Русский

Если r ∈ nonZeroDivisorsRight R, то x r = y r эквивалентно x = y.

LaTeX

$$$$\\operatorname{IsRightRegular}(r) \\text{ or } r \\in \\text{nonZeroDivisorsRight } R \\Rightarrow (x r = y r \\iff x = y)$$$$

Lean4

theorem mul_cancel_right_mem_nonZeroDivisorsRight (hr : r ∈ nonZeroDivisorsRight R) : x * r = y * r ↔ x = y :=
  ⟨(isRightRegular_iff_mem_nonZeroDivisorsRight.mpr hr ·), congr_arg (· * r)⟩

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