no goals
M : Type u_1
M' : Type ?u.10326
M₁ : Type ?u.10329
R : Type ?u.10332
R' : Type ?u.10335
F : Type ?u.10338
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x r : M
hr : r ∈ M⁰
⊢ x = 0 → x * r = 0
simp (config := { contextual := true })