R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y + y) ^ p = x ^ p
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p
rw [eq_sub_iff_add_eq, ← add_pow_char_of_commute _ _ _ (Commute.sub_left h rfl)]
no goals
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y + y) ^ p = x ^ p
simp