# mathlibdocumentation

algebra.char_p.basic

# Characteristic of semirings #

theorem char_p_iff (R : Type u) (p : ) :
p ∀ (x : ), x = 0 p x
@[class]
structure char_p (R : Type u) (p : ) :
Prop

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

Warning: for a semiring R, char_p R 0 and char_zero R need not coincide.

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

For instance, endowing {0, 1} with addition given by max (i.e. 1 is absorbing), shows that char_zero {0, 1} does not hold and yet char_p {0, 1} 0 does. This example is formalized in counterexamples/char_p_zero_ne_char_zero.

Instances of this typeclass
theorem char_p.cast_eq_zero (R : Type u) (p : ) [ p] :
p = 0
@[simp]
theorem char_p.cast_card_eq_zero (R : Type u) [fintype R] :
theorem char_p.add_order_of_one (R : Type u_1) [semiring R] :
theorem char_p.int_cast_eq_zero_iff (R : Type u) (p : ) [ p] (a : ) :
a = 0 p a
theorem char_p.int_coe_eq_int_coe_iff (R : Type u) (p : ) [ p] (a b : ) :
theorem char_p.eq (R : Type u) {p q : } (c1 : p) (c2 : q) :
p = q
@[protected, instance]
def char_p.of_char_zero (R : Type u) [char_zero R] :
0
theorem char_p.exists (R : Type u)  :
∃ (p : ), p
theorem char_p.exists_unique (R : Type u)  :
∃! (p : ), p
theorem char_p.congr {R : Type u} {p : } (q : ) [hq : q] (h : q = p) :
p
noncomputable def ring_char (R : Type u)  :

Noncomputable function that outputs the unique characteristic of a semiring.

Equations
Instances for ring_char
theorem ring_char.spec (R : Type u) (x : ) :
x = 0 x
theorem ring_char.eq (R : Type u) (p : ) [C : p] :
= p
@[protected, instance]
def ring_char.char_p (R : Type u)  :
theorem ring_char.of_eq {R : Type u} {p : } (h : = p) :
p
theorem ring_char.eq_iff {R : Type u} {p : } :
= p p
theorem ring_char.dvd {R : Type u} {x : } (hx : x = 0) :
x
@[simp]
theorem ring_char.eq_zero {R : Type u} [char_zero R] :
= 0
@[simp]
theorem ring_char.nat.cast_ring_char {R : Type u}  :
theorem add_pow_char_of_commute (R : Type u) [semiring R] {p : } [fact (nat.prime p)] [ p] (x y : R) (h : y) :
(x + y) ^ p = x ^ p + y ^ p
theorem add_pow_char_pow_of_commute (R : Type u) [semiring R] {p : } [fact (nat.prime p)] [ p] {n : } (x y : R) (h : y) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
theorem sub_pow_char_of_commute (R : Type u) [ring R] {p : } [fact (nat.prime p)] [ p] (x y : R) (h : y) :
(x - y) ^ p = x ^ p - y ^ p
theorem sub_pow_char_pow_of_commute (R : Type u) [ring R] {p : } [fact (nat.prime p)] [ p] {n : } (x y : R) (h : y) :
(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
theorem add_pow_char (R : Type u) {p : } [fact (nat.prime p)] [ p] (x y : R) :
(x + y) ^ p = x ^ p + y ^ p
theorem add_pow_char_pow (R : Type u) {p : } [fact (nat.prime p)] [ p] {n : } (x y : R) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
theorem sub_pow_char (R : Type u) [comm_ring R] {p : } [fact (nat.prime p)] [ p] (x y : R) :
(x - y) ^ p = x ^ p - y ^ p
theorem sub_pow_char_pow (R : Type u) [comm_ring R] {p : } [fact (nat.prime p)] [ p] {n : } (x y : R) :
(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
theorem eq_iff_modeq_int (R : Type u) [ring R] (p : ) [ p] (a b : ) :
theorem char_p.neg_one_ne_one (R : Type u) [ring R] (p : ) [ p] [fact (2 < p)] :
-1 1
theorem char_p.neg_one_pow_char (R : Type u) [comm_ring R] (p : ) [ p] [fact (nat.prime p)] :
(-1) ^ p = -1
theorem char_p.neg_one_pow_char_pow (R : Type u) [comm_ring R] (p n : ) [ p] [fact (nat.prime p)] :
(-1) ^ p ^ n = -1
theorem ring_hom.char_p_iff_char_p {K : Type u_1} {L : Type u_2} [semiring L] [nontrivial L] (f : K →+* L) (p : ) :
p p
def frobenius (R : Type u) (p : ) [fact (nat.prime p)] [ p] :
R →+* R

The frobenius map that sends x to x^p

Equations
theorem frobenius_def {R : Type u} (p : ) [fact (nat.prime p)] [ p] (x : R) :
p) x = x ^ p
theorem iterate_frobenius {R : Type u} (p : ) [fact (nat.prime p)] [ p] (x : R) (n : ) :
p)^[n] x = x ^ p ^ n
theorem frobenius_mul {R : Type u} (p : ) [fact (nat.prime p)] [ p] (x y : R) :
p) (x * y) = p) x * p) y
theorem frobenius_one {R : Type u} (p : ) [fact (nat.prime p)] [ p] :
p) 1 = 1
theorem monoid_hom.map_frobenius {R : Type u} {S : Type v} (f : R →* S) (p : ) [fact (nat.prime p)] [ p] [ p] (x : R) :
f ( p) x) = p) (f x)
theorem ring_hom.map_frobenius {R : Type u} {S : Type v} (g : R →+* S) (p : ) [fact (nat.prime p)] [ p] [ p] (x : R) :
g ( p) x) = p) (g x)
theorem monoid_hom.map_iterate_frobenius {R : Type u} {S : Type v} (f : R →* S) (p : ) [fact (nat.prime p)] [ p] [ p] (x : R) (n : ) :
f ( p)^[n] x) = p)^[n] (f x)
theorem ring_hom.map_iterate_frobenius {R : Type u} {S : Type v} (g : R →+* S) (p : ) [fact (nat.prime p)] [ p] [ p] (x : R) (n : ) :
g ( p)^[n] x) = p)^[n] (g x)
theorem monoid_hom.iterate_map_frobenius {R : Type u} (x : R) (f : R →* R) (p : ) [fact (nat.prime p)] [ p] (n : ) :
f^[n] ( p) x) = p) (f^[n] x)
theorem ring_hom.iterate_map_frobenius {R : Type u} (x : R) (f : R →+* R) (p : ) [fact (nat.prime p)] [ p] (n : ) :
f^[n] ( p) x) = p) (f^[n] x)
theorem frobenius_zero (R : Type u) (p : ) [fact (nat.prime p)] [ p] :
p) 0 = 0
theorem frobenius_add (R : Type u) (p : ) [fact (nat.prime p)] [ p] (x y : R) :
p) (x + y) = p) x + p) y
theorem frobenius_nat_cast (R : Type u) (p : ) [fact (nat.prime p)] [ p] (n : ) :
p) n = n
theorem list_sum_pow_char {R : Type u} (p : ) [fact (nat.prime p)] [ p] (l : list R) :
l.sum ^ p = (list.map (λ (_x : R), _x ^ p) l).sum
theorem multiset_sum_pow_char {R : Type u} (p : ) [fact (nat.prime p)] [ p] (s : multiset R) :
s.sum ^ p = (multiset.map (λ (_x : R), _x ^ p) s).sum
theorem sum_pow_char {R : Type u} (p : ) [fact (nat.prime p)] [ p] {ι : Type u_1} (s : finset ι) (f : ι → R) :
s.sum (λ (i : ι), f i) ^ p = s.sum (λ (i : ι), f i ^ p)
theorem frobenius_neg (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] (x : R) :
p) (-x) = - p) x
theorem frobenius_sub (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] (x y : R) :
p) (x - y) = p) x - p) y
theorem frobenius_inj (R : Type u) [comm_ring R] [is_reduced R] (p : ) [fact (nat.prime p)] [ p] :
theorem is_square_of_char_two' {R : Type u_1} [finite R] [comm_ring R] [is_reduced R] [ 2] (a : R) :

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

theorem char_p.char_p_to_char_zero (R : Type u_1) [ 0] :
theorem char_p.cast_eq_mod (R : Type u) (p : ) [ p] (k : ) :
k = (k % p)
theorem char_p.char_ne_zero_of_finite (R : Type u) (p : ) [ p] [finite R] :
p 0

The characteristic of a finite ring cannot be zero.

theorem char_p.ring_char_ne_zero_of_finite (R : Type u) [finite R] :
0
@[simp]
theorem char_p.pow_prime_pow_mul_eq_one_iff {R : Type u} [comm_ring R] [is_reduced R] (p k m : ) [fact (nat.prime p)] [ p] (x : R) :
x ^ (p ^ k * m) = 1 x ^ m = 1
theorem char_p.char_ne_one (R : Type u) [nontrivial R] (p : ) [hc : p] :
p 1
theorem char_p.char_is_prime_of_two_le (R : Type u) (p : ) [hc : p] (hp : 2 p) :
theorem char_p.char_is_prime_or_zero (R : Type u) [nontrivial R] (p : ) [hc : p] :
p = 0
theorem char_p.char_is_prime_of_pos (R : Type u) [nontrivial R] (p : ) [ne_zero p] [ p] :
theorem char_p.char_is_prime (R : Type u) [ring R] [nontrivial R] [finite R] (p : ) [ p] :
@[protected, instance]
def char_p.subsingleton {R : Type u} [ 1] :
theorem char_p.ring_char_ne_one {R : Type u} [nontrivial R] :
1
theorem char_p.nontrivial_of_char_ne_one {R : Type u} {v : } (hv : v 1) [hr : v] :
theorem char_p.ring_char_of_prime_eq_zero {R : Type u} [nontrivial R] {p : } (hprime : nat.prime p) (hp0 : p = 0) :
= p
@[protected]
theorem ring.two_ne_zero {R : Type u_1} [nontrivial R] (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_1} [nontrivial R] (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_1} [nontrivial R] (hR : 2) {a : R} :
-a = a a = 0

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

theorem char_p_of_ne_zero (R : Type u) [fintype R] (n : ) (hn : = n) (hR : ∀ (i : ), i < ni = 0i = 0) :
n
theorem char_p_of_prime_pow_injective (R : Type u_1) [ring R] [fintype R] (p : ) [hp : fact (nat.prime p)] (n : ) (hn : = p ^ n) (hR : ∀ (i : ), i np ^ i = 0i = n) :
(p ^ n)
@[protected, instance]
def nat.lcm.char_p (R : Type u) (S : Type v) [semiring R] [semiring S] (p q : ) [ p] [ q] :
char_p (R × S) (p.lcm q)

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

@[protected, instance]
def prod.char_p (R : Type u) (S : Type v) [semiring R] [semiring S] (p : ) [ p] [ p] :
char_p (R × S) p

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

theorem int.cast_inj_on_of_ring_char_ne_two {R : Type u_1} [nontrivial R] (hR : 2) :
{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 ne_zero.of_not_dvd (R : Type u) {n p : } [ p] (h : ¬p n) :
theorem ne_zero.not_char_dvd (R : Type u) (p : ) [ p] (k : ) [h : ne_zero k] :
¬p k