Documentation

Mathlib.Algebra.CharP.Basic

Characteristic of semirings #

theorem Commute.add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : } {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * kFinset.Ioo 0 (p ^ n), 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 : Nat.Prime p) (h : Commute x y) :
(x + y) ^ p = x ^ p + y ^ p + p * kFinset.Ioo 0 p, 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 : Nat.Prime p) (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 : Nat.Prime p) (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 : Nat.Prime p) (x : R) (y : R) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * kFinset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ((p ^ n).choose k / p)
theorem add_pow_prime_eq {R : Type u_1} [CommSemiring R] {p : } (hp : Nat.Prime p) (x : R) (y : R) :
(x + y) ^ p = x ^ p + y ^ p + p * kFinset.Ioo 0 p, x ^ k * y ^ (p - k) * (p.choose k / p)
theorem exists_add_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : } (hp : Nat.Prime p) (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 : Nat.Prime p) (x : R) (y : R) :
∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + p * r
theorem add_pow_char_of_commute (R : Type u_1) [Semiring R] {p : } [hp : Fact (Nat.Prime p)] [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 (Nat.Prime p)] [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 (Nat.Prime p)] [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 (Nat.Prime p)] [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 (Nat.Prime p)] [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 (Nat.Prime p)] [CharP R p] {n : } (x : R) (y : R) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
theorem add_pow_eq_add_pow_mod_mul_pow_add_pow_div (R : Type u_1) [CommSemiring R] {p : } [Fact (Nat.Prime p)] [CharP R p] {n : } (x : R) (y : R) :
(x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
theorem sub_pow_char (R : Type u_1) [CommRing R] {p : } [Fact (Nat.Prime p)] [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 (Nat.Prime p)] [CharP R p] {n : } (x : R) (y : R) :
(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
theorem sub_pow_eq_sub_pow_mod_mul_pow_sub_pow_div (R : Type u_1) [CommRing R] {p : } [Fact (Nat.Prime p)] [CharP R p] {n : } (x : R) (y : R) :
(x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
theorem CharP.neg_one_pow_char (R : Type u_1) [Ring R] (p : ) [CharP R p] [Fact (Nat.Prime p)] :
(-1) ^ p = -1
theorem CharP.neg_one_pow_char_pow (R : Type u_1) [Ring R] (p : ) (n : ) [CharP R p] [Fact (Nat.Prime p)] :
(-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.char_is_prime (R : Type u_1) [Ring R] [NoZeroDivisors R] [Nontrivial R] [Finite R] (p : ) [CharP R p] :