R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) x - ↑(frobenius R p) h = 0
⊢ x - h = 0
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H : ↑(frobenius R p) x = ↑(frobenius R p) h
⊢ x = h
rw [← sub_eq_zero] at H⊢
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) (x - h) = 0
⊢ x - h = 0
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) x - ↑(frobenius R p) h = 0
⊢ x - h = 0
rw [← frobenius_sub] at H
no goals
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) (x - h) = 0
⊢ x - h = 0
exact IsReduced.eq_zero _ ⟨_, H⟩