LeanPool.EcTateLean.Algebra.CharP.Basic

Imported Lean Pool material for LeanPool.EcTateLean.Algebra.CharP.Basic.

theorem ringChar_is_zero_or_prime (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] : ringChar R = 0 ∨ Nat.Prime (ringChar R)

theorem add_pow_ringChar {R : Type u_1} [CommRing R] [IsDomain R] (a b : R) (h : ringChar R ≠ 0) : (a + b) ^ ringChar R = a ^ ringChar R + b ^ ringChar R

theorem sub_pow_ringChar {R : Type u_1} [CommRing R] [IsDomain R] (a b : R) (h : ringChar R ≠ 0) : (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R

theorem pow_ringChar_injective {R : Type u_1} [CommRing R] [IsDomain R] (hn : ringChar R ≠ 0) : Function.Injective fun (x : R) => x ^ ringChar R