R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h✝ : ↑n * a = ↑n * b
h : ↑n = 0 ∨ a = b
⊢ n = 0 ∨ a = b
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
⊢ n = 0 ∨ a = b
rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h
no goals
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h✝ : ↑n * a = ↑n * b
h : ↑n = 0 ∨ a = b
⊢ n = 0 ∨ a = b
exact_mod_cast h