no goals
M : Type ?u.12943
M' : Type ?u.12946
M₁ : Type u_1
R : Type ?u.12952
R' : Type ?u.12955
F : Type ?u.12958
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
r x : M₁
hr : r ∈ M₁⁰
⊢ r * x = 0 ↔ x = 0
rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]