doc-next-gen

Mathlib.Algebra.CharP.Lemmas

Module docstring

{"# Characteristic of semirings "}

Commute.add_pow_prime_pow_eq theorem
(h : Commute x y) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
Full source 
protected theorem add_pow_prime_pow_eq (h : Commute x y) (n : ℕ) :
    (x + y) ^ p ^ n =
      x ^ p ^ n + y ^ p ^ n +
        p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) := by
  trans x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (p ^ n).choose k
  · simp_rw [h.add_pow, ← Nat.Ico_zero_eq_range, Nat.Ico_succ_right, Icc_eq_cons_Ico (zero_le _),
      Finset.sum_cons, Ico_eq_cons_Ioo (pow_pos hp.pos _), Finset.sum_cons, tsub_self, tsub_zero,
      pow_zero, Nat.choose_zero_right, Nat.choose_self, Nat.cast_one, mul_one, one_mul, ← add_assoc]
  · congr 1
    simp_rw [Finset.mul_sum, Nat.cast_comm, mul_assoc _ _ (p : R), ← Nat.cast_mul]
    refine Finset.sum_congr rfl fun i hi => ?_
    rw [mem_Ioo] at hi
    rw [Nat.div_mul_cancel (hp.dvd_choose_pow hi.1.ne' hi.2.ne)]
Binomial Expansion Modulo $p$ for Commuting Elements: $(x + y)^{p^n} \equiv x^{p^n} + y^{p^n} \mod p$
Informal description
Let $x$ and $y$ be elements in a semiring that commute (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n} + p \cdot \sum_{k \in (0, p^n)} x^k y^{p^n - k} \cdot \left\lfloor \frac{\binom{p^n}{k}}{p} \right\rfloor \] where the sum is taken over all integers $k$ strictly between $0$ and $p^n$.
Commute.add_pow_prime_eq theorem
(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)
Full source 
protected theorem add_pow_prime_eq (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) := by
  simpa using h.add_pow_prime_pow_eq hp 1
Binomial Expansion Modulo $p$ for Commuting Elements: $(x + y)^p \equiv x^p + y^p \mod p$
Informal description
Let $x$ and $y$ be elements in a semiring that commute (i.e., $xy = yx$), and let $p$ be a prime number. Then the following identity holds: \[ (x + y)^p = x^p + y^p + p \cdot \sum_{k \in (0, p)} x^k y^{p - k} \cdot \left\lfloor \frac{\binom{p}{k}}{p} \right\rfloor \] where the sum is taken over all integers $k$ strictly between $0$ and $p$.
Commute.exists_add_pow_prime_pow_eq theorem
(h : Commute x y) (n : ℕ) : ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r
Full source 
protected theorem exists_add_pow_prime_pow_eq (h : Commute x y) (n : ℕ) :
    ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r :=
  ⟨_, h.add_pow_prime_pow_eq hp n⟩
Existence of Remainder in Prime Power Binomial Expansion for Commuting Elements
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, there exists an element $r$ in the semiring such that: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n} + p \cdot r \]
Commute.exists_add_pow_prime_eq theorem
(h : Commute x y) : ∃ r, (x + y) ^ p = x ^ p + y ^ p + p * r
Full source 
protected theorem exists_add_pow_prime_eq (h : Commute x y) :
    ∃ r, (x + y) ^ p = x ^ p + y ^ p + p * r :=
  ⟨_, h.add_pow_prime_eq hp⟩
Existence of Remainder in Prime Binomial Expansion for Commuting Elements
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then there exists an element $r$ in the semiring such that: \[ (x + y)^p = x^p + y^p + p \cdot r \]
add_pow_prime_pow_eq theorem
: (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)
Full source 
theorem add_pow_prime_pow_eq :
    (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) :=
  (Commute.all x y).add_pow_prime_pow_eq hp n
Binomial Expansion Modulo $p$: $(x + y)^{p^n} \equiv x^{p^n} + y^{p^n} \mod p$
Informal description
Let $x$ and $y$ be elements in a commutative semiring, and let $p$ be a prime number. For any natural number $n$, the following identity holds: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n} + p \cdot \sum_{k \in (0, p^n)} x^k y^{p^n - k} \cdot \left\lfloor \frac{\binom{p^n}{k}}{p} \right\rfloor \] where the sum is taken over all integers $k$ strictly between $0$ and $p^n$.
add_pow_prime_eq theorem
: (x + y) ^ p = x ^ p + y ^ p + p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
Full source 
theorem add_pow_prime_eq :
    (x + y) ^ p =
      x ^ p + y ^ p + p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p) :=
  (Commute.all x y).add_pow_prime_eq hp
Binomial Expansion Modulo $p$: $(x + y)^p \equiv x^p + y^p \mod p$
Informal description
Let $x$ and $y$ be elements in a commutative semiring, and let $p$ be a prime number. Then the following identity holds: \[ (x + y)^p = x^p + y^p + p \cdot \sum_{k \in (0, p)} x^k y^{p - k} \cdot \left\lfloor \frac{\binom{p}{k}}{p} \right\rfloor \] where the sum is taken over all integers $k$ strictly between $0$ and $p$.
exists_add_pow_prime_pow_eq theorem
: ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r
Full source 
theorem exists_add_pow_prime_pow_eq :
    ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r :=
  (Commute.all x y).exists_add_pow_prime_pow_eq hp n
Existence of Remainder in Prime Power Binomial Expansion for Commuting Elements
Informal description
Let $x$ and $y$ be elements in a commutative semiring, and let $p$ be a prime number. For any natural number $n$, there exists an element $r$ in the semiring such that: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n} + p \cdot r. \]
exists_add_pow_prime_eq theorem
: ∃ r, (x + y) ^ p = x ^ p + y ^ p + p * r
Full source 
theorem exists_add_pow_prime_eq :
    ∃ r, (x + y) ^ p = x ^ p + y ^ p + p * r :=
  (Commute.all x y).exists_add_pow_prime_eq hp
Existence of Remainder in Prime Binomial Expansion for Commuting Elements
Informal description
Let $x$ and $y$ be elements in a commutative semiring, and let $p$ be a prime number. Then there exists an element $r$ in the semiring such that: \[ (x + y)^p = x^p + y^p + p \cdot r. \]
add_pow_expChar_of_commute theorem
(h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p
Full source 
lemma add_pow_expChar_of_commute (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p := by
  obtain _ | hprime := hR
  · simp only [pow_one]
  · let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hprime
    simp [hr]
Prime Binomial Theorem for Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then the following identity holds: \[ (x + y)^p = x^p + y^p. \]
add_pow_expChar_pow_of_commute theorem
(h : Commute x y) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Full source 
lemma add_pow_expChar_pow_of_commute (h : Commute x y) :
    (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n := by
  obtain _ | hprime := hR
  · simp only [one_pow, pow_one]
  · let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hprime n
    simp [hr]
Prime Power Binomial Theorem for Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n} \]
add_pow_eq_mul_pow_add_pow_div_expChar_of_commute theorem
(h : Commute x y) : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
Full source 
lemma add_pow_eq_mul_pow_add_pow_div_expChar_of_commute (h : Commute x y) :
    (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p) := by
  rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
Generalized Prime Binomial Theorem for Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x + y)^n = (x + y)^{n \bmod p} \cdot (x^p + y^p)^{\lfloor n/p \rfloor}. \]
add_pow_char_of_commute theorem
(h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p
Full source 
lemma add_pow_char_of_commute (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p :=
  add_pow_expChar_of_commute _ h
Prime Binomial Theorem for Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then the following identity holds: \[ (x + y)^p = x^p + y^p. \]
add_pow_char_pow_of_commute theorem
(h : Commute x y) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Full source 
lemma add_pow_char_pow_of_commute (h : Commute x y) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n :=
  add_pow_expChar_pow_of_commute _ _ h
Prime Power Binomial Theorem for Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n} \]
add_pow_eq_mul_pow_add_pow_div_char_of_commute theorem
(h : Commute x y) : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
Full source 
lemma add_pow_eq_mul_pow_add_pow_div_char_of_commute (h : Commute x y) :
    (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p) :=
  add_pow_eq_mul_pow_add_pow_div_expChar_of_commute _ _ h
Generalized Prime Binomial Theorem for Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x + y)^n = (x + y)^{n \bmod p} \cdot (x^p + y^p)^{\lfloor n/p \rfloor}. \]
add_pow_expChar theorem
: (x + y) ^ p = x ^ p + y ^ p
Full source 
lemma add_pow_expChar : (x + y) ^ p = x ^ p + y ^ p := add_pow_expChar_of_commute _ <| .all ..
Prime Binomial Theorem in Commutative Semirings
Informal description
Let $p$ be a prime number. For any elements $x$ and $y$ in a commutative semiring, the following identity holds: \[ (x + y)^p = x^p + y^p. \]
add_pow_expChar_pow theorem
: (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Full source 
lemma add_pow_expChar_pow : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n :=
  add_pow_expChar_pow_of_commute _ _ <| .all ..
Prime Power Binomial Theorem in Commutative Semirings
Informal description
Let $p$ be a prime number and $n$ a natural number. For any elements $x$ and $y$ in a commutative semiring, the following identity holds: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n}. \]
add_pow_eq_mul_pow_add_pow_div_expChar theorem
: (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
Full source 
lemma add_pow_eq_mul_pow_add_pow_div_expChar :
    (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p) :=
  add_pow_eq_mul_pow_add_pow_div_expChar_of_commute _ _ <| .all ..
Generalized Prime Binomial Theorem in Commutative Semirings
Informal description
Let $p$ be a prime number. For any elements $x$ and $y$ in a commutative semiring and any natural number $n$, the following identity holds: \[ (x + y)^n = (x + y)^{n \bmod p} \cdot (x^p + y^p)^{\lfloor n/p \rfloor}. \]
add_pow_char theorem
: (x + y) ^ p = x ^ p + y ^ p
Full source 
lemma add_pow_char : (x + y) ^ p = x ^ p + y ^ p := add_pow_expChar ..
Prime Binomial Theorem in Commutative Semirings
Informal description
Let $p$ be a prime number. For any elements $x$ and $y$ in a commutative semiring, the following identity holds: \[ (x + y)^p = x^p + y^p. \]
add_pow_char_pow theorem
: (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Full source 
lemma add_pow_char_pow : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n := add_pow_expChar_pow ..
Prime Power Binomial Theorem in Commutative Semirings
Informal description
Let $p$ be a prime number and $n$ a natural number. For any elements $x$ and $y$ in a commutative semiring, the following identity holds: \[ (x + y)^{p^n} = x^{p^n} + y^{p^n}. \]
add_pow_eq_mul_pow_add_pow_div_char theorem
: (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
Full source 
lemma add_pow_eq_mul_pow_add_pow_div_char :
    (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p) :=
  add_pow_eq_mul_pow_add_pow_div_expChar ..
Generalized Prime Binomial Theorem in Commutative Semirings
Informal description
Let $p$ be a prime number. For any elements $x$ and $y$ in a commutative semiring and any natural number $n$, the following identity holds: \[ (x + y)^n = (x + y)^{n \bmod p} \cdot (x^p + y^p)^{\lfloor n/p \rfloor}. \]
sub_pow_expChar_of_commute theorem
(h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p
Full source 
lemma sub_pow_expChar_of_commute (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p := by
  simp [eq_sub_iff_add_eq, ← add_pow_expChar_of_commute _ (h.sub_left rfl)]
Prime Binomial Theorem for Differences of Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then the following identity holds: \[ (x - y)^p = x^p - y^p. \]
sub_pow_expChar_pow_of_commute theorem
(h : Commute x y) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
Full source 
lemma sub_pow_expChar_pow_of_commute (h : Commute x y) :
    (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n := by
  simp [eq_sub_iff_add_eq, ← add_pow_expChar_pow_of_commute _ _ (h.sub_left rfl)]
Prime Power Binomial Theorem for Differences of Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x - y)^{p^n} = x^{p^n} - y^{p^n} \]
sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute theorem
(h : Commute x y) : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
Full source 
lemma sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute (h : Commute x y) :
    (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p) := by
  rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
Generalized Binomial Theorem for Differences of Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x - y)^n = (x - y)^{n \bmod p} \cdot (x^p - y^p)^{\lfloor n/p \rfloor}. \]
neg_one_pow_expChar_pow theorem
: (-1 : R) ^ p ^ n = -1
Full source 
lemma neg_one_pow_expChar_pow : (-1 : R) ^ p ^ n = -1 := by
  rw [eq_neg_iff_add_eq_zero]
  nth_rw 2 [← one_pow (p ^ n)]
  rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]
Power of Negative One in Semirings: $(-1)^{p^n} = -1$
Informal description
For any prime power $p^n$ in a semiring $R$, the power of $-1$ raised to $p^n$ equals $-1$, i.e., $(-1)^{p^n} = -1$.
sub_pow_char_of_commute theorem
(h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p
Full source 
lemma sub_pow_char_of_commute (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p :=
  sub_pow_expChar_of_commute _ h
Prime Binomial Theorem for Differences of Commuting Elements in Semirings
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then the following identity holds: \[ (x - y)^p = x^p - y^p. \]
sub_pow_char_pow_of_commute theorem
(h : Commute x y) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
Full source 
lemma sub_pow_char_pow_of_commute (h : Commute x y) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n :=
  sub_pow_expChar_pow_of_commute _ _ h
Prime power binomial theorem for differences of commuting elements
Informal description
Let $x$ and $y$ be commuting elements in a semiring (i.e., $xy = yx$), and let $p$ be a prime number. Then for any natural number $n$, the following identity holds: \[ (x - y)^{p^n} = x^{p^n} - y^{p^n}. \]
neg_one_pow_char theorem
: (-1 : R) ^ p = -1
Full source 
lemma neg_one_pow_char : (-1 : R) ^ p = -1 := neg_one_pow_expChar ..
Power of Negative One in Characteristic $p$: $(-1)^p = -1$
Informal description
Let $R$ be a ring of characteristic $p$, where $p$ is a prime number. Then $(-1)^p = -1$ in $R$.
neg_one_pow_char_pow theorem
: (-1 : R) ^ p ^ n = -1
Full source 
lemma neg_one_pow_char_pow : (-1 : R) ^ p ^ n = -1 := neg_one_pow_expChar_pow ..
Power of negative one in characteristic $p^n$: $(-1)^{p^n} = -1$
Informal description
Let $R$ be a ring with characteristic $p^n$ where $p$ is a prime number and $n$ is a natural number. Then $(-1)^{p^n} = -1$ in $R$.
sub_pow_eq_mul_pow_sub_pow_div_char_of_commute theorem
(h : Commute x y) : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
Full source 
lemma sub_pow_eq_mul_pow_sub_pow_div_char_of_commute (h : Commute x y) :
    (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p) :=
  sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute _ _ h
Generalized binomial theorem for commuting elements in characteristic $p$: $(x - y)^n = (x - y)^{n \bmod p} \cdot (x^p - y^p)^{\lfloor n/p \rfloor}$
Informal description
Let $R$ be a semiring of characteristic $p$ (where $p$ is a prime), and let $x, y \in R$ be commuting elements (i.e., $xy = yx$). Then for any natural number $n$, the following identity holds: \[ (x - y)^n = (x - y)^{n \bmod p} \cdot (x^p - y^p)^{\lfloor n/p \rfloor}. \]
sub_pow_expChar theorem
: (x - y) ^ p = x ^ p - y ^ p
Full source 
lemma sub_pow_expChar : (x - y) ^ p = x ^ p - y ^ p := sub_pow_expChar_of_commute _ <| .all ..
Binomial theorem in characteristic $p$: $(x - y)^p = x^p - y^p$
Informal description
Let $R$ be a commutative ring of characteristic $p$ (where $p$ is a prime). For any elements $x, y \in R$, the following identity holds: \[ (x - y)^p = x^p - y^p. \]
sub_pow_expChar_pow theorem
: (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
Full source 
lemma sub_pow_expChar_pow : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n :=
  sub_pow_expChar_pow_of_commute _ _ <| .all ..
Prime Power Binomial Theorem in Characteristic $p$
Informal description
Let $x$ and $y$ be elements in a commutative ring of characteristic $p$ (where $p$ is a prime). Then for any natural number $n$, the following identity holds: \[ (x - y)^{p^n} = x^{p^n} - y^{p^n}. \]
sub_pow_eq_mul_pow_sub_pow_div_expChar theorem
: (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
Full source 
lemma sub_pow_eq_mul_pow_sub_pow_div_expChar :
    (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p) :=
  sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute _ _ <| .all ..
Generalized Binomial Theorem in Characteristic $p$: $(x-y)^n = (x-y)^{n \bmod p} \cdot (x^p - y^p)^{\lfloor n/p \rfloor}$
Informal description
Let $R$ be a commutative ring of characteristic $p$ (where $p$ is a prime). For any elements $x, y \in R$ and any natural number $n$, the following identity holds: \[ (x - y)^n = (x - y)^{n \bmod p} \cdot (x^p - y^p)^{\lfloor n/p \rfloor}. \]
sub_pow_char theorem
: (x - y) ^ p = x ^ p - y ^ p
Full source 
lemma sub_pow_char : (x - y) ^ p = x ^ p - y ^ p := sub_pow_expChar ..
Binomial theorem in characteristic $p$: $(x - y)^p = x^p - y^p$
Informal description
Let $R$ be a commutative ring of characteristic $p$ (where $p$ is a prime). For any elements $x, y \in R$, the following identity holds: \[ (x - y)^p = x^p - y^p. \]
sub_pow_char_pow theorem
: (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
Full source 
lemma sub_pow_char_pow : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n := sub_pow_expChar_pow ..
Prime Power Binomial Theorem in Characteristic $p$
Informal description
Let $R$ be a commutative ring of characteristic $p$ (where $p$ is a prime). Then for any elements $x, y \in R$ and any natural number $n$, we have the identity: \[ (x - y)^{p^n} = x^{p^n} - y^{p^n}. \]
sub_pow_eq_mul_pow_sub_pow_div_char theorem
: (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
Full source 
lemma sub_pow_eq_mul_pow_sub_pow_div_char :
    (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p) :=
  sub_pow_eq_mul_pow_sub_pow_div_expChar ..
Generalized binomial theorem in characteristic $p$: $(x-y)^n = (x-y)^{n \bmod p} \cdot (x^p - y^p)^{\lfloor n/p \rfloor}$
Informal description
Let $R$ be a commutative ring of characteristic $p$ (where $p$ is a prime). For any elements $x, y \in R$ and any natural number $n$, the following identity holds: \[ (x - y)^n = (x - y)^{n \bmod p} \cdot (x^p - y^p)^{\lfloor n/p \rfloor}. \]
Nat.Prime.dvd_add_pow_sub_pow_of_dvd theorem
(hpri : p.Prime) {r : R} (h₁ : r ∣ x ^ p) (h₂ : r ∣ p * x) : r ∣ (x + y) ^ p - y ^ p
Full source 
lemma Nat.Prime.dvd_add_pow_sub_pow_of_dvd (hpri : p.Prime) {r : R} (h₁ : r ∣ x ^ p)
    (h₂ : r ∣ p * x) : r ∣ (x + y) ^ p - y ^ p := by
  rw [add_pow_prime_eq hpri, add_right_comm, add_assoc, add_sub_assoc, add_sub_cancel_right]
  apply dvd_add h₁ (h₂.trans <| mul_dvd_mul_left _ <| Finset.dvd_sum _)
  simp only [Finset.mem_Ioo, and_imp, mul_assoc]
  intro i hi0 _
  exact dvd_mul_of_dvd_left (dvd_rfl.pow hi0.ne') _
Divisibility of $(x + y)^p - y^p$ by $r$ when $r$ divides $x^p$ and $p \cdot x$ in a commutative semiring of characteristic $p$
Informal description
Let $p$ be a prime number and $R$ a commutative semiring. For any elements $x, y \in R$ and any $r \in R$, if $r$ divides $x^p$ and $r$ divides $p \cdot x$, then $r$ divides $(x + y)^p - y^p$.
CharP.char_ne_zero_of_finite theorem
(p : ℕ) [CharP R p] [Finite R] : p ≠ 0
Full source 
/-- The characteristic of a finite ring cannot be zero. -/
theorem char_ne_zero_of_finite (p : ℕ) [CharP R p] [Finite R] : p ≠ 0 := by
  rintro rfl
  haveI : CharZero R := charP_to_charZero R
  cases nonempty_fintype R
  exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))
Nonzero Characteristic of Finite Semirings
Informal description
For any semiring $R$ of finite cardinality and any natural number $p$, if $R$ has characteristic $p$ (i.e., $p$ is the smallest positive natural number such that $p \cdot 1 = 0$ in $R$), then $p$ cannot be zero.
CharP.char_is_prime theorem
(p : ℕ) [CharP R p] : p.Prime
Full source 
theorem char_is_prime (p : ℕ) [CharP R p] : p.Prime :=
  Or.resolve_right (char_is_prime_or_zero R p) (char_ne_zero_of_finite R p)
Characteristic of a Semiring is Prime
Informal description
For any semiring $R$ with characteristic $p$ (i.e., the smallest positive natural number such that $p \cdot 1 = 0$ in $R$), the characteristic $p$ must be a prime number.
frobenius definition
: R →+* R
Full source 
/-- The Frobenius map `x ↦ x ^ p`. -/
def frobenius : R →+* R where
  __ := powMonoidHom p
  map_zero' := zero_pow (expChar_pos R p).ne'
  map_add' _ _ := add_pow_expChar ..
Frobenius endomorphism
Informal description
The Frobenius endomorphism on a commutative semiring \( R \) of characteristic exponent \( p \) is the ring homomorphism \( \text{Frob}_p : R \to R \) defined by \( x \mapsto x^p \). It preserves both the additive and multiplicative structures of \( R \), satisfying: - \( \text{Frob}_p(x + y) = \text{Frob}_p(x) + \text{Frob}_p(y) \) (additivity) - \( \text{Frob}_p(x \cdot y) = \text{Frob}_p(x) \cdot \text{Frob}_p(y) \) (multiplicativity) - \( \text{Frob}_p(0) = 0 \) (preservation of zero) - \( \text{Frob}_p(1) = 1 \) (preservation of multiplicative identity)
iterateFrobenius definition
: R →+* R
Full source 
/-- The iterated Frobenius map `x ↦ x ^ p ^ n`. -/
def iterateFrobenius : R →+* R where
  __ := powMonoidHom (p ^ n)
  map_zero' := zero_pow (expChar_pow_pos R p n).ne'
  map_add' _ _ := add_pow_expChar_pow ..
Iterated Frobenius homomorphism
Informal description
The iterated Frobenius map \( \text{Frob}_{p^n} : R \to R \) is a semiring homomorphism defined by \( x \mapsto x^{p^n} \), where \( p \) is the characteristic exponent of the semiring \( R \) and \( n \) is a natural number. This map preserves both the additive and multiplicative structures of \( R \).
list_sum_pow_char theorem
(l : List R) : l.sum ^ p = (l.map (· ^ p : R → R)).sum
Full source 
lemma list_sum_pow_char (l : List R) : l.sum ^ p = (l.map (· ^ p : R → R)).sum :=
  map_list_sum (frobenius R p) _
Frobenius Endomorphism on List Sums: $(\sum x)^p = \sum x^p$
Informal description
For any list $l$ of elements in a commutative semiring $R$ of characteristic exponent $p$, the $p$-th power of the sum of the elements in $l$ is equal to the sum of the $p$-th powers of the elements in $l$. That is, \[ \left( \sum_{x \in l} x \right)^p = \sum_{x \in l} x^p. \]
multiset_sum_pow_char theorem
(s : Multiset R) : s.sum ^ p = (s.map (· ^ p : R → R)).sum
Full source 
lemma multiset_sum_pow_char (s : Multiset R) : s.sum ^ p = (s.map (· ^ p : R → R)).sum :=
  map_multiset_sum (frobenius R p) _
Power of Sum Equals Sum of Powers in Characteristic $p$ for Multisets
Informal description
Let $R$ be a commutative semiring of characteristic exponent $p$. For any multiset $s$ of elements in $R$, the sum of the elements in $s$ raised to the power $p$ equals the sum of each element in $s$ raised to the power $p$. In symbols: $$ \left(\sum_{x \in s} x\right)^p = \sum_{x \in s} x^p $$
sum_pow_char theorem
{ι : Type*} (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ p = ∑ i ∈ s, f i ^ p
Full source 
lemma sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ p = ∑ i ∈ s, f i ^ p :=
  map_sum (frobenius R p) _ _
Frobenius Identity for Finite Sums: $(\sum f)^p = \sum f^p$
Informal description
Let $R$ be a commutative semiring of characteristic exponent $p$. For any finite set $s$ and any function $f : \iota \to R$, the $p$-th power of the sum of $f$ over $s$ equals the sum of the $p$-th powers of $f$ over $s$. In symbols: $$ \left( \sum_{i \in s} f(i) \right)^p = \sum_{i \in s} f(i)^p. $$
list_sum_pow_char_pow theorem
(l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum
Full source 
lemma list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum :=
  map_list_sum (iterateFrobenius R p n) _
Power of Sum Equals Sum of Powers in Characteristic $p^n$ for Lists
Informal description
Let $R$ be a commutative semiring of characteristic exponent $p$ (i.e., $p$ is the smallest positive integer such that $x \mapsto x^p$ is a semiring endomorphism). For any list $l$ of elements in $R$ and any natural number $n$, the sum of the elements in $l$ raised to the power $p^n$ equals the sum of each element in $l$ raised to the power $p^n$. In symbols: $$ \left(\sum_{x \in l} x\right)^{p^n} = \sum_{x \in l} x^{p^n} $$
multiset_sum_pow_char_pow theorem
(s : Multiset R) : s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum
Full source 
lemma multiset_sum_pow_char_pow (s : Multiset R) :
    s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum :=
  map_multiset_sum (iterateFrobenius R p n) _
Multiset Sum Power Identity in Characteristic $p$: $(\sum x)^{p^n} = \sum x^{p^n}$
Informal description
Let $R$ be a commutative semiring of characteristic exponent $p$ and let $n$ be a natural number. For any multiset $s$ over $R$, the $p^n$-th power of the sum of elements in $s$ equals the sum of the $p^n$-th powers of the elements in $s$. In symbols: $$ \left( \sum_{x \in s} x \right)^{p^n} = \sum_{x \in s} x^{p^n}. $$
sum_pow_char_pow theorem
{ι : Type*} (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ p ^ n = ∑ i ∈ s, f i ^ p ^ n
Full source 
lemma sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
    (∑ i ∈ s, f i) ^ p ^ n = ∑ i ∈ s, f i ^ p ^ n := map_sum (iterateFrobenius R p n) _ _
Sum of Powers in Characteristic $p$ Semiring: $(\sum f)^{p^n} = \sum f^{p^n}$
Informal description
Let $R$ be a commutative semiring of characteristic exponent $p$, and let $n$ be a natural number. For any finite set $s$ and function $f : \iota \to R$, the sum of $f$ over $s$ raised to the power $p^n$ equals the sum of each $f(i)$ raised to the power $p^n$ over $s$. That is, \[ \left( \sum_{i \in s} f(i) \right)^{p^n} = \sum_{i \in s} f(i)^{p^n}. \]