Non-zero divisors in a ring

theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_1} [Ring R] {x y r : R} (hr : r ∈ nonZeroDivisors R) : x * r = y * r ↔ x = y

theorem mul_cancel_right_coe_nonZeroDivisors {R : Type u_1} [Ring R] {x y : R} {c : ↥(nonZeroDivisors R)} : x * ↑c = y * ↑c ↔ x = y

theorem isUnit_iff_mem_nonZeroDivisors_of_finite {R : Type u_1} [Ring R] {a : R} [Finite R] : IsUnit a ↔ a ∈ nonZeroDivisors R

In a finite ring, an element is a unit iff it is a non-zero-divisor.

@[simp]

theorem mul_cancel_left_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {r x y : R} (hr : r ∈ nonZeroDivisors R) : r * x = r * y ↔ x = y

theorem mul_cancel_left_coe_nonZeroDivisors {R : Type u_1} [CommRing R] {x y : R} {c : ↥(nonZeroDivisors R)} : ↑c * x = ↑c * y ↔ x = y

theorem dvd_cancel_right_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {r x y : R} (hr : r ∈ nonZeroDivisors R) : x * r ∣ y * r ↔ x ∣ y

theorem dvd_cancel_right_coe_nonZeroDivisors {R : Type u_1} [CommRing R] {x y : R} {c : ↥(nonZeroDivisors R)} : x * ↑c ∣ y * ↑c ↔ x ∣ y

theorem dvd_cancel_left_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {r x y : R} (hr : r ∈ nonZeroDivisors R) : r * x ∣ r * y ↔ x ∣ y

theorem dvd_cancel_left_coe_nonZeroDivisors {R : Type u_1} [CommRing R] {x y : R} {c : ↥(nonZeroDivisors R)} : ↑c * x ∣ ↑c * y ↔ x ∣ y