exact add_pow_char _ _ _
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
no goals