Theorem: sub_pow_ringChar (ECTate/Algebra/CharP/Basic.lean)

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Tactic:
have : NeZero (ringChar R) := ⟨h⟩
State after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this : NeZero (ringChar R)
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this : NeZero (ringChar R)
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Tactic:
have := CharP.char_is_prime_of_pos R (ringChar R)
State after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this✝ : NeZero (ringChar R)
this : Fact (Nat.Prime (ringChar R))
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this✝ : NeZero (ringChar R)
this : Fact (Nat.Prime (ringChar R))
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Tactic:
exact sub_pow_char _ _ _
State after:
no goals