R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0
R : Type u
inst✝ : EuclideanDomain R
b d : R
ha : b * d ≠ 0
⊢ d = 0 → b * d = 0
rintro rfl
no goals
R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0
exact mul_zero _