Characteristic of semirings

theorem Commute.add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : ℕ} (hp : Nat.Prime p) {x : R} {y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.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 : ℕ} (hp : Nat.Prime p) {x : R} {y : R} (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.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 : ℕ} (hp : Nat.Prime p) {x : R} {y : R} (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 : ℕ} (hp : Nat.Prime p) {x : R} {y : R} (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 * ∑ k ∈ Finset.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 * ∑ k ∈ Finset.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_expChar_of_commute {R : Type u_1} [Semiring R] {x : R} {y : R} (p : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p

theorem add_pow_expChar_pow_of_commute {R : Type u_1} [Semiring R] {x : R} {y : R} (p : ℕ) (n : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

theorem add_pow_eq_mul_pow_add_pow_div_expChar_of_commute {R : Type u_1} [Semiring R] {x : R} {y : R} (p : ℕ) (n : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

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

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

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

theorem add_pow_expChar {R : Type u_1} [CommSemiring R] (x : R) (y : R) (p : ℕ) [hR : ExpChar R p] : (x + y) ^ p = x ^ p + y ^ p

theorem add_pow_expChar_pow {R : Type u_1} [CommSemiring R] (x : R) (y : R) (p : ℕ) (n : ℕ) [hR : ExpChar R p] : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

theorem add_pow_eq_mul_pow_add_pow_div_expChar {R : Type u_1} [CommSemiring R] (x : R) (y : R) (p : ℕ) (n : ℕ) [hR : ExpChar R p] : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

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

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

theorem add_pow_eq_mul_pow_add_pow_div_char {R : Type u_1} [CommSemiring R] (x : R) (y : R) (p : ℕ) (n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

@[deprecated add_pow_eq_mul_pow_add_pow_div_char]

theorem add_pow_eq_add_pow_mod_mul_pow_add_pow_div {R : Type u_1} [CommSemiring R] (x : R) (y : R) (p : ℕ) (n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Alias of add_pow_eq_mul_pow_add_pow_div_char.

theorem sub_pow_expChar_of_commute {R : Type u_1} [Ring R] {x : R} {y : R} (p : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p

theorem sub_pow_expChar_pow_of_commute {R : Type u_1} [Ring R] {x : R} {y : R} (p : ℕ) (n : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

theorem sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute {R : Type u_1} [Ring R] {x : R} {y : R} (p : ℕ) (n : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

theorem neg_one_pow_expChar (R : Type u_1) [Ring R] (p : ℕ) [hR : ExpChar R p] : (-1) ^ p = -1

theorem neg_one_pow_expChar_pow (R : Type u_1) [Ring R] (p : ℕ) (n : ℕ) [hR : ExpChar R p] : (-1) ^ p ^ n = -1

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

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

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

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

theorem sub_pow_eq_mul_pow_sub_pow_div_char_of_commute (R : Type u_1) [Ring R] {x : R} {y : R} (p : ℕ) (n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] (h : Commute x y) : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

theorem sub_pow_expChar {R : Type u_1} [CommRing R] (x : R) (y : R) {p : ℕ} [hR : ExpChar R p] : (x - y) ^ p = x ^ p - y ^ p

theorem sub_pow_expChar_pow {R : Type u_1} [CommRing R] (x : R) (y : R) (n : ℕ) {p : ℕ} [hR : ExpChar R p] : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

theorem sub_pow_eq_mul_pow_sub_pow_div_expChar {R : Type u_1} [CommRing R] (x : R) (y : R) (n : ℕ) {p : ℕ} [hR : ExpChar R p] : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

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

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

theorem sub_pow_eq_mul_pow_sub_pow_div_char {R : Type u_1} [CommRing R] (x : R) (y : R) (n : ℕ) {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

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] : Nat.Prime p

The Frobenius automorphism

def frobenius (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] : R →+* R

The frobenius map x ↦ x ^ p.

Equations

• frobenius R p = { toMonoidHom := powMonoidHom p, map_zero' := ⋯, map_add' := ⋯ }

def iterateFrobenius (R : Type u_1) [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] : R →+* R

The iterated frobenius map x ↦ x ^ p ^ n.

Equations

• iterateFrobenius R p n = { toMonoidHom := powMonoidHom (p ^ n), map_zero' := ⋯, map_add' := ⋯ }

theorem frobenius_def {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) : (frobenius R p) x = x ^ p

theorem iterateFrobenius_def {R : Type u_1} [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p n) x = x ^ p ^ n

theorem iterate_frobenius {R : Type u_1} [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (⇑(frobenius R p))^[n] x = x ^ p ^ n

theorem coe_iterateFrobenius (R : Type u_1) [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] : ⇑(iterateFrobenius R p n) = (⇑(frobenius R p))^[n]

theorem iterateFrobenius_one_apply (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p 1) x = x ^ p

@[simp]

theorem iterateFrobenius_one (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] : iterateFrobenius R p 1 = frobenius R p

theorem iterateFrobenius_zero_apply (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p 0) x = x

@[simp]

theorem iterateFrobenius_zero (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] : iterateFrobenius R p 0 = RingHom.id R

theorem iterateFrobenius_add_apply (R : Type u_1) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

theorem iterateFrobenius_add (R : Type u_1) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] : iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n)

theorem iterateFrobenius_mul_apply (R : Type u_1) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x

theorem coe_iterateFrobenius_mul (R : Type u_1) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] : ⇑(iterateFrobenius R p (m * n)) = (⇑(iterateFrobenius R p m))^[n]

theorem frobenius_mul {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) (y : R) : (frobenius R p) (x * y) = (frobenius R p) x * (frobenius R p) y

theorem frobenius_one {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] : (frobenius R p) 1 = 1

theorem MonoidHom.map_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) : f ((frobenius R p) x) = (frobenius S p) (f x)

theorem RingHom.map_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) : g ((frobenius R p) x) = (frobenius S p) (g x)

theorem MonoidHom.map_iterate_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) : f ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (f x)

theorem RingHom.map_iterate_frobenius {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) : g ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (g x)

theorem MonoidHom.iterate_map_frobenius {R : Type u_1} [CommSemiring R] (x : R) (f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) : (⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)

theorem RingHom.iterate_map_frobenius {R : Type u_1} [CommSemiring R] (x : R) (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) : (⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)

theorem list_sum_pow_char {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (l : List R) : l.sum ^ p = (List.map (fun (x : R) => x ^ p) l).sum

theorem multiset_sum_pow_char {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (s : Multiset R) : s.sum ^ p = (Multiset.map (fun (x : R) => x ^ p) s).sum

theorem sum_pow_char {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] {ι : Type u_4} (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ p = ∑ i ∈ s, f i ^ p

theorem list_sum_pow_char_pow {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) (l : List R) : l.sum ^ p ^ n = (List.map (fun (x : R) => x ^ p ^ n) l).sum

theorem multiset_sum_pow_char_pow {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) (s : Multiset R) : s.sum ^ p ^ n = (Multiset.map (fun (x : R) => x ^ p ^ n) s).sum

theorem sum_pow_char_pow {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) {ι : Type u_4} (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ p ^ n = ∑ i ∈ s, f i ^ p ^ n

theorem frobenius_neg {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (x : R) : (frobenius R p) (-x) = -(frobenius R p) x

theorem frobenius_sub {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (x : R) (y : R) : (frobenius R p) (x - y) = (frobenius R p) x - (frobenius R p) y