algebra.char_p

# Characteristic of semirings

@[class]
structure char_p (α : Type u) [semiring α] :
→ Prop

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

Instances
theorem char_p.cast_eq_zero (α : Type u) [semiring α] (p : ) [ p] :
p = 0

@[simp]
theorem char_p.cast_card_eq_zero (R : Type u_1) [ring R] [fintype R] :

theorem char_p.int_cast_eq_zero_iff (R : Type u) [ring R] (p : ) [ p] (a : ) :
a = 0 p a

theorem char_p.int_coe_eq_int_coe_iff (R : Type u_1) [ring R] (p : ) [ p] (a b : ) :

theorem char_p.eq (α : Type u) [semiring α] {p q : } :
p qp = q

@[instance]
def char_p.of_char_zero (α : Type u) [semiring α] [char_zero α] :
0

theorem char_p.exists (α : Type u) [semiring α] :
∃ (p : ), p

theorem char_p.exists_unique (α : Type u) [semiring α] :
∃! (p : ), p

def ring_char (α : Type u) [semiring α] :

Noncomputable function that outputs the unique characteristic of a semiring.

Equations
theorem ring_char.spec (α : Type u) [semiring α] (x : ) :
x = 0 x

theorem ring_char.eq (α : Type u) [semiring α] {p : } :
pp =

theorem add_pow_char_of_commute (R : Type u) [ring R] {p : } [fact (nat.prime p)] [ p] (x y : R) :
y(x + y) ^ p = x ^ p + y ^ p

theorem add_pow_char_pow_of_commute (R : Type u) [ring R] {p : } [fact (nat.prime p)] [ p] {n : } (x y : R) :
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) :
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) :
y(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

theorem add_pow_char (α : Type u) [comm_ring α] {p : } [fact (nat.prime p)] [ p] (x y : α) :
(x + y) ^ p = x ^ p + y ^ p

theorem add_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 sub_pow_char (α : Type u) [comm_ring α] {p : } [fact (nat.prime p)] [ p] (x y : α) :
(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_1) [ring R] (p : ) [ p] (a b : ) :

theorem char_p.neg_one_ne_one (R : Type u_1) [ring R] (p : ) [ p] [fact (2 < p)] :
-1 1

theorem ring_hom.char_p_iff_char_p {K : Type u_1} {L : Type u_2} [field K] [field L] (f : K →+* L) (p : ) :
p p

def frobenius (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] :
R →+* R

The frobenius map that sends x to x^p

Equations
theorem frobenius_def {R : Type u} [comm_ring R] (p : ) [fact (nat.prime p)] [ p] (x : R) :
p) x = x ^ p

theorem iterate_frobenius {R : Type u} [comm_ring R] (p : ) [fact (nat.prime p)] [ p] (x : R) (n : ) :
p)^[n] x = x ^ p ^ n

theorem frobenius_mul {R : Type u} [comm_ring R] (p : ) [fact (nat.prime p)] [ p] (x y : R) :
p) (x * y) = ( p) x) * p) y

theorem frobenius_one {R : Type u} [comm_ring R] (p : ) [fact (nat.prime p)] [ p] :
p) 1 = 1

theorem monoid_hom.map_frobenius {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (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} [comm_ring R] {S : Type v} [comm_ring S] (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} [comm_ring R] {S : Type v} [comm_ring S] (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} [comm_ring R] {S : Type v} [comm_ring S] (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} [comm_ring R] (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} [comm_ring R] (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) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] :
p) 0 = 0

theorem frobenius_add (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] (x y : R) :
p) (x + y) = p) x + p) y

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_nat_cast (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] (n : ) :
p) n = n

theorem frobenius_inj (α : Type u) (p : ) [fact (nat.prime p)] [ p] :

theorem char_p.char_p_to_char_zero (α : Type u) [ring α] [ 0] :

theorem char_p.cast_eq_mod (α : Type u) [ring α] (p : ) [ p] (k : ) :
k = (k % p)

theorem char_p.char_ne_zero_of_fintype (α : Type u) [ring α] (p : ) [hc : p] [fintype α] :
p 0

theorem char_p.char_ne_one (α : Type u) (p : ) [hc : p] :
p 1

theorem char_p.char_is_prime_of_two_le (α : Type u) (p : ) [hc : p] :
2 p

theorem char_p.char_is_prime_or_zero (α : Type u) (p : ) [hc : p] :
p = 0

theorem char_p.char_is_prime_of_pos (α : Type u) (p : ) [h : fact (0 < p)] [ p] :

theorem char_p.char_is_prime (α : Type u) [fintype α] (p : ) [ p] :

@[instance]
def char_p.subsingleton {R : Type u_1} [semiring R] [ 1] :

theorem char_p.false_of_nontrivial_of_char_one {R : Type u_1} [semiring R] [nontrivial R] [ 1] :

theorem char_p.ring_char_ne_one {R : Type u_1} [semiring R] [nontrivial R] :
1

theorem char_p.nontrivial_of_char_ne_one {v : } (hv : v 1) {R : Type u_1} [semiring R] [hr : v] :

theorem char_p_of_ne_zero (n : ) (R : Type u_1) [comm_ring R] [fintype R] :
(∀ (i : ), i < ni = 0i = 0) n

theorem char_p_of_prime_pow_injective (R : Type u_1) [comm_ring R] [fintype R] (p : ) [hp : fact (nat.prime p)] (n : ) :
= p ^ n(∀ (i : ), i np ^ i = 0i = n) (p ^ n)