exact pow_eq_zero h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ : x ^ ringChar R - y ^ ringChar R = 0
h : (x - y) ^ ringChar R = 0
⊢ x - y = 0
no goals