Characteristic of semirings

theorem Commute.add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : p.Prime) (h : Commute x y) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * (Finset.Ioo 0 (p ^ n)).sum fun (k : ℕ) => x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

theorem Commute.add_pow_prime_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : p.Prime) (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p + ↑p * (Finset.Ioo 0 p).sum fun (k : ℕ) => x ^ k * y ^ (p - k) * ↑(p.choose k / p)

theorem Commute.exists_add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : p.Prime) (h : Commute x y) (n : ℕ) : ∃ (r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r

theorem Commute.exists_add_pow_prime_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : p.Prime) (h : Commute x y) : ∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + ↑p * r

theorem add_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : p.Prime) (x : R) (y : R) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * (Finset.Ioo 0 (p ^ n)).sum fun (k : ℕ) => x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

theorem add_pow_prime_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : p.Prime) (x : R) (y : R) : (x + y) ^ p = x ^ p + y ^ p + ↑p * (Finset.Ioo 0 p).sum fun (k : ℕ) => x ^ k * y ^ (p - k) * ↑(p.choose k / p)

theorem exists_add_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : p.Prime) (x : R) (y : R) (n : ℕ) : ∃ (r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r

theorem exists_add_pow_prime_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : p.Prime) (x : R) (y : R) : ∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + ↑p * r

@[simp]

theorem CharP.cast_card_eq_zero (R : Type u_1) [AddGroupWithOne R] [Fintype R] : ↑(Fintype.card R) = 0

theorem CharP.addOrderOf_one (R : Type u_2) [Semiring R] : CharP R (addOrderOf 1)

theorem add_pow_char_of_commute (R : Type u_1) [Semiring R] {p : ℕ} [hp : Fact p.Prime] [CharP R p] (x : R) (y : R) (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p

theorem add_pow_char_pow_of_commute (R : Type u_1) [Semiring R] {p : ℕ} {n : ℕ} [hp : Fact p.Prime] [CharP R p] (x : R) (y : R) (h : Commute x y) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

theorem sub_pow_char_of_commute (R : Type u_1) [Ring R] {p : ℕ} [Fact p.Prime] [CharP R p] (x : R) (y : R) (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p

theorem sub_pow_char_pow_of_commute (R : Type u_1) [Ring R] {p : ℕ} [Fact p.Prime] [CharP R p] {n : ℕ} (x : R) (y : R) (h : Commute x y) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

theorem add_pow_char (R : Type u_1) [CommSemiring R] {p : ℕ} [Fact p.Prime] [CharP R p] (x : R) (y : R) : (x + y) ^ p = x ^ p + y ^ p

theorem add_pow_char_pow (R : Type u_1) [CommSemiring R] {p : ℕ} [Fact p.Prime] [CharP R p] {n : ℕ} (x : R) (y : R) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

theorem sub_pow_char (R : Type u_1) [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] (x : R) (y : R) : (x - y) ^ p = x ^ p - y ^ p

theorem sub_pow_char_pow (R : Type u_1) [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] {n : ℕ} (x : R) (y : R) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

theorem CharP.neg_one_pow_char (R : Type u_1) [Ring R] (p : ℕ) [CharP R p] [Fact p.Prime] : (-1) ^ p = -1

theorem CharP.neg_one_pow_char_pow (R : Type u_1) [Ring R] (p : ℕ) (n : ℕ) [CharP R p] [Fact p.Prime] : (-1) ^ p ^ n = -1

theorem CharP.char_ne_zero_of_finite (R : Type u_1) [NonAssocRing R] (p : ℕ) [CharP R p] [Finite R] : p ≠ 0

The characteristic of a finite ring cannot be zero.

theorem CharP.ringChar_ne_zero_of_finite (R : Type u_1) [NonAssocRing R] [Finite R] : ringChar R ≠ 0

theorem CharP.char_is_prime (R : Type u_1) [Ring R] [NoZeroDivisors R] [Nontrivial R] [Finite R] (p : ℕ) [CharP R p] : p.Prime

theorem charP_of_ne_zero (R : Type u_1) [NonAssocRing R] [Fintype R] (n : ℕ) (hn : Fintype.card R = n) (hR : ∀ i < n, ↑i = 0 → i = 0) : CharP R n

theorem charP_of_prime_pow_injective (R : Type u_2) [Ring R] [Fintype R] (p : ℕ) [hp : Fact p.Prime] (n : ℕ) (hn : Fintype.card R = p ^ n) (hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n) : CharP R (p ^ n)