# Documentation

Mathlib.Algebra.CharP.Basic

# Characteristic of semirings #

theorem Commute.add_pow_prime_pow_eq {R : Type u_1} [] {p : } {x : R} {y : R} (hp : ) (h : Commute x y) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * Finset.sum (Finset.Ioo 0 (p ^ n)) fun k => x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
theorem Commute.add_pow_prime_eq {R : Type u_1} [] {p : } {x : R} {y : R} (hp : ) (h : Commute x y) :
(x + y) ^ p = x ^ p + y ^ p + p * Finset.sum () fun k => x ^ k * y ^ (p - k) * ↑( / p)
theorem Commute.exists_add_pow_prime_pow_eq {R : Type u_1} [] {p : } {x : R} {y : R} (hp : ) (h : Commute x y) (n : ) :
r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r
theorem Commute.exists_add_pow_prime_eq {R : Type u_1} [] {p : } {x : R} {y : R} (hp : ) (h : Commute x y) :
r, (x + y) ^ p = x ^ p + y ^ p + p * r
theorem add_pow_prime_pow_eq {R : Type u_1} [] {p : } (hp : ) (x : R) (y : R) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * Finset.sum (Finset.Ioo 0 (p ^ n)) fun k => x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
theorem add_pow_prime_eq {R : Type u_1} [] {p : } (hp : ) (x : R) (y : R) :
(x + y) ^ p = x ^ p + y ^ p + p * Finset.sum () fun k => x ^ k * y ^ (p - k) * ↑( / p)
theorem exists_add_pow_prime_pow_eq {R : Type u_1} [] {p : } (hp : ) (x : R) (y : R) (n : ) :
r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r
theorem exists_add_pow_prime_eq {R : Type u_1} [] {p : } (hp : ) (x : R) (y : R) :
r, (x + y) ^ p = x ^ p + y ^ p + p * r
theorem charP_iff (R : Type u_1) [] (p : ) :
CharP R p ∀ (x : ), x = 0 p x
class CharP (R : Type u_1) [] (p : ) :
• cast_eq_zero_iff' : ∀ (x : ), x = 0 p x

The generator of the kernel of the unique homomorphism ℕ → R for a semiring R.

Warning: for a semiring R, CharP R 0 and CharZero R need not coincide.

• CharP R 0 asks that only 0 : ℕ maps to 0 : R under the map ℕ → R;
• CharZero R requires an injection ℕ ↪ R.

For instance, endowing {0, 1} with addition given by max (i.e. 1 is absorbing), shows that CharZero {0, 1} does not hold and yet CharP {0, 1} 0 does. This example is formalized in Counterexamples/CharPZeroNeCharZero.lean.

Instances
theorem CharP.cast_eq_zero_iff (R : Type u) [] (p : ) [CharP R p] (x : ) :
x = 0 p x
@[simp]
theorem CharP.cast_eq_zero (R : Type u_1) [] (p : ) [CharP R p] :
p = 0
@[simp]
theorem CharP.cast_card_eq_zero (R : Type u_1) [] [] :
↑() = 0
theorem CharP.addOrderOf_one (R : Type u_2) [] :
CharP R ()
theorem CharP.int_cast_eq_zero_iff (R : Type u_1) [] (p : ) [CharP R p] (a : ) :
a = 0 p a
theorem CharP.intCast_eq_intCast (R : Type u_1) [] (p : ) [CharP R p] {a : } {b : } :
a = b a b [ZMOD p]
theorem CharP.natCast_eq_natCast (R : Type u_1) [] (p : ) [CharP R p] {a : } {b : } :
a = b a b [MOD p]
theorem CharP.eq (R : Type u_1) [] {p : } {q : } (_c1 : CharP R p) (_c2 : CharP R q) :
p = q
instance CharP.ofCharZero (R : Type u_1) [] [] :
CharP R 0
theorem CharP.exists (R : Type u_1) [] :
p, CharP R p
theorem CharP.exists_unique (R : Type u_1) [] :
∃! p, CharP R p
theorem CharP.congr {R : Type u} [] {p : } (q : ) [hq : CharP R q] (h : q = p) :
CharP R p
noncomputable def ringChar (R : Type u_1) [] :

Noncomputable function that outputs the unique characteristic of a semiring.

Instances For
theorem ringChar.spec (R : Type u_1) [] (x : ) :
x = 0 x
theorem ringChar.eq (R : Type u_1) [] (p : ) [C : CharP R p] :
= p
instance ringChar.charP (R : Type u_1) [] :
CharP R ()
theorem ringChar.of_eq {R : Type u_1} [] {p : } (h : = p) :
CharP R p
theorem ringChar.eq_iff {R : Type u_1} [] {p : } :
= p CharP R p
theorem ringChar.dvd {R : Type u_1} [] {x : } (hx : x = 0) :
x
@[simp]
theorem ringChar.eq_zero {R : Type u_1} [] [] :
= 0
theorem ringChar.Nat.cast_ringChar {R : Type u_1} [] :
↑() = 0
theorem add_pow_char_of_commute (R : Type u_1) [] {p : } [hp : Fact ()] [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) [] {p : } {n : } [hp : Fact ()] [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 ()] [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 ()] [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) [] {p : } [Fact ()] [CharP R p] (x : R) (y : R) :
(x + y) ^ p = x ^ p + y ^ p
theorem add_pow_char_pow (R : Type u_1) [] {p : } [Fact ()] [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) [] {p : } [Fact ()] [CharP R p] (x : R) (y : R) :
(x - y) ^ p = x ^ p - y ^ p
theorem sub_pow_char_pow (R : Type u_1) [] {p : } [Fact ()] [CharP R p] {n : } (x : R) (y : R) :
(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
theorem CharP.neg_one_ne_one (R : Type u_1) [Ring R] (p : ) [CharP R p] [Fact (2 < p)] :
-1 1
theorem CharP.neg_one_pow_char (R : Type u_1) [] (p : ) [CharP R p] [Fact ()] :
(-1) ^ p = -1
theorem CharP.neg_one_pow_char_pow (R : Type u_1) [] (p : ) (n : ) [CharP R p] [Fact ()] :
(-1) ^ p ^ n = -1
theorem RingHom.charP_iff_charP {K : Type u_2} {L : Type u_3} [] [] [] (f : K →+* L) (p : ) :
CharP K p CharP L p
def frobenius (R : Type u_1) [] (p : ) [Fact ()] [CharP R p] :
R →+* R

The frobenius map that sends x to x^p

Instances For
theorem frobenius_def {R : Type u_1} [] (p : ) [Fact ()] [CharP R p] (x : R) :
↑() x = x ^ p
theorem iterate_frobenius {R : Type u_1} [] (p : ) [Fact ()] [CharP R p] (x : R) (n : ) :
))^[n] x = x ^ p ^ n
theorem frobenius_mul {R : Type u_1} [] (p : ) [Fact ()] [CharP R p] (x : R) (y : R) :
↑() (x * y) = ↑() x * ↑() y
theorem frobenius_one {R : Type u_1} [] (p : ) [Fact ()] [CharP R p] :
↑() 1 = 1
theorem MonoidHom.map_frobenius {R : Type u_1} [] {S : Type v} [] (f : R →* S) (p : ) [Fact ()] [CharP R p] [CharP S p] (x : R) :
f (↑() x) = ↑() (f x)
theorem RingHom.map_frobenius {R : Type u_1} [] {S : Type v} [] (g : R →+* S) (p : ) [Fact ()] [CharP R p] [CharP S p] (x : R) :
g (↑() x) = ↑() (g x)
theorem MonoidHom.map_iterate_frobenius {R : Type u_1} [] {S : Type v} [] (f : R →* S) (p : ) [Fact ()] [CharP R p] [CharP S p] (x : R) (n : ) :
f ())^[n] x) = ))^[n] (f x)
theorem RingHom.map_iterate_frobenius {R : Type u_1} [] {S : Type v} [] (g : R →+* S) (p : ) [Fact ()] [CharP R p] [CharP S p] (x : R) (n : ) :
g ())^[n] x) = ))^[n] (g x)
theorem MonoidHom.iterate_map_frobenius {R : Type u_1} [] (x : R) (f : R →* R) (p : ) [Fact ()] [CharP R p] (n : ) :
(f)^[n] (↑() x) = ↑() ((f)^[n] x)
theorem RingHom.iterate_map_frobenius {R : Type u_1} [] (x : R) (f : R →+* R) (p : ) [Fact ()] [CharP R p] (n : ) :
(f)^[n] (↑() x) = ↑() ((f)^[n] x)
theorem frobenius_zero (R : Type u_1) [] (p : ) [Fact ()] [CharP R p] :
↑() 0 = 0
theorem frobenius_add (R : Type u_1) [] (p : ) [Fact ()] [CharP R p] (x : R) (y : R) :
↑() (x + y) = ↑() x + ↑() y
theorem frobenius_nat_cast (R : Type u_1) [] (p : ) [Fact ()] [CharP R p] (n : ) :
↑() n = n
theorem list_sum_pow_char {R : Type u_1} [] (p : ) [Fact ()] [CharP R p] (l : List R) :
^ p = List.sum (List.map (fun x => x ^ p) l)
theorem multiset_sum_pow_char {R : Type u_1} [] (p : ) [Fact ()] [CharP R p] (s : ) :
= Multiset.sum (Multiset.map (fun x => x ^ p) s)
theorem sum_pow_char {R : Type u_1} [] (p : ) [Fact ()] [CharP R p] {ι : Type u_2} (s : ) (f : ιR) :
(Finset.sum s fun i => f i) ^ p = Finset.sum s fun i => f i ^ p
theorem frobenius_neg (R : Type u_1) [] (p : ) [Fact ()] [CharP R p] (x : R) :
↑() (-x) = -↑() x
theorem frobenius_sub (R : Type u_1) [] (p : ) [Fact ()] [CharP R p] (x : R) (y : R) :
↑() (x - y) = ↑() x - ↑() y
theorem frobenius_inj (R : Type u_1) [] [] (p : ) [Fact ()] [CharP R p] :
theorem isSquare_of_charTwo' {R : Type u_2} [] [] [] [CharP R 2] (a : R) :

If ringChar R = 2, where R is a finite reduced commutative ring, then every a : R is a square.

theorem CharP.charP_to_charZero (R : Type u_2) [] [CharP R 0] :
theorem CharP.cast_eq_mod (R : Type u_1) [] (p : ) [CharP R p] (k : ) :
k = ↑(k % p)
theorem CharP.char_ne_zero_of_finite (R : Type u_1) [] (p : ) [CharP R p] [] :
p 0

The characteristic of a finite ring cannot be zero.

theorem CharP.ringChar_ne_zero_of_finite (R : Type u_1) [] [] :
0
@[simp]
theorem CharP.pow_prime_pow_mul_eq_one_iff {R : Type u_1} [] [] (p : ) (k : ) (m : ) [Fact ()] [CharP R p] (x : R) :
x ^ (p ^ k * m) = 1 x ^ m = 1
theorem CharP.char_ne_one (R : Type u_1) [] [] (p : ) [hc : CharP R p] :
p 1
theorem CharP.char_is_prime_of_two_le (R : Type u_1) [] [] (p : ) [hc : CharP R p] (hp : 2 p) :
theorem CharP.char_is_prime_or_zero (R : Type u_1) [] [] [] (p : ) [hc : CharP R p] :
p = 0
theorem CharP.char_is_prime_of_pos (R : Type u_1) [] [] [] (p : ) [] [CharP R p] :
Fact ()
theorem CharP.char_is_prime (R : Type u_1) [Ring R] [] [] [] (p : ) [CharP R p] :
instance CharP.CharOne.subsingleton {R : Type u_1} [] [CharP R 1] :
theorem CharP.ringChar_ne_one {R : Type u_1} [] [] :
1
theorem CharP.nontrivial_of_char_ne_one {R : Type u_1} [] {v : } (hv : v 1) [hr : CharP R v] :
theorem CharP.ringChar_of_prime_eq_zero {R : Type u_1} [] [] {p : } (hprime : ) (hp0 : p = 0) :
= p
theorem CharP.charP_iff_prime_eq_zero {R : Type u_1} [] [] {p : } (hp : ) :
CharP R p p = 0
theorem Ring.two_ne_zero {R : Type u_2} [] [] (hR : 2) :
2 0

We have 2 ≠ 0 in a nontrivial ring whose characteristic is not 2.

theorem Ring.neg_one_ne_one_of_char_ne_two {R : Type u_2} [] [] (hR : 2) :
-1 1

Characteristic ≠ 2 and nontrivial implies that -1 ≠ 1.

theorem Ring.eq_self_iff_eq_zero_of_char_ne_two {R : Type u_2} [] [] [] (hR : 2) {a : R} :
-a = a a = 0

Characteristic ≠ 2 in a domain implies that -a = a iff a = 0.

theorem charP_of_ne_zero (R : Type u_1) [] [] (n : ) (hn : ) (hR : ∀ (i : ), i < ni = 0i = 0) :
CharP R n
theorem charP_of_prime_pow_injective (R : Type u_2) [Ring R] [] (p : ) [hp : Fact ()] (n : ) (hn : = p ^ n) (hR : ∀ (i : ), i np ^ i = 0i = n) :
CharP R (p ^ n)
instance Nat.lcm.charP (R : Type u_1) (S : Type v) [] [] (p : ) (q : ) [CharP R p] [CharP S q] :
CharP (R × S) (Nat.lcm p q)

The characteristic of the product of rings is the least common multiple of the characteristics of the two rings.

instance Prod.charP (R : Type u_1) (S : Type v) [] [] (p : ) [CharP R p] [CharP S p] :
CharP (R × S) p

The characteristic of the product of two rings of the same characteristic is the same as the characteristic of the rings

instance ULift.charP (R : Type u_1) [] (p : ) [CharP R p] :
CharP () p
instance MulOpposite.charP (R : Type u_1) [] (p : ) [CharP R p] :
theorem Int.cast_injOn_of_ringChar_ne_two {R : Type u_2} [] [] (hR : 2) :
Set.InjOn Int.cast {0, 1, -1}

If two integers from {0, 1, -1} result in equal elements in a ring R that is nontrivial and of characteristic not 2, then they are equal.

theorem NeZero.of_not_dvd (R : Type u_1) [] {n : } {p : } [CharP R p] (h : ¬p n) :
NeZero n
theorem NeZero.not_char_dvd (R : Type u_1) [] (p : ) [CharP R p] (k : ) [h : NeZero k] :
¬p k
theorem CharZero.charZero_iff_forall_prime_ne_zero (R : Type u_1) [] [] [] :
∀ (p : ), p 0