mathlib documentation

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 : ) [char_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 : ) [char_p R p] (a : ) :
a = 0 p a

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

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

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

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

theorem char_p.exists_unique (α : Type u) [semiring α] :
∃! (p : ), char_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 : ) :

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

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

theorem add_pow_char (α : Type u) [comm_ring α] {p : } [fact (nat.prime p)] [char_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)] [char_p R 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)] [char_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)] [char_p R 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 : ) [char_p R p] (a b : ) :

theorem char_p.neg_one_ne_one (R : Type u_1) [ring R] (p : ) [char_p R 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 : ) :
char_p K p char_p L p

def frobenius (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R 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)] [char_p R p] (x : R) :
(frobenius R p) x = x ^ p

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

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

theorem frobenius_one {R : Type u} [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R p] :
(frobenius R 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)] [char_p R p] [char_p S p] (x : R) :
f ((frobenius R p) x) = (frobenius S 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)] [char_p R p] [char_p S p] (x : R) :
g ((frobenius R p) x) = (frobenius S 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)] [char_p R p] [char_p S p] (x : R) (n : ) :
f ((frobenius R p)^[n] x) = (frobenius S 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)] [char_p R p] [char_p S p] (x : R) (n : ) :
g ((frobenius R p)^[n] x) = (frobenius S 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)] [char_p R p] (n : ) :
f^[n] ((frobenius R p) x) = (frobenius R 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)] [char_p R p] (n : ) :
f^[n] ((frobenius R p) x) = (frobenius R p) (f^[n] x)

theorem frobenius_zero (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R p] :
(frobenius R p) 0 = 0

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

theorem frobenius_neg (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R p] (x : R) :
(frobenius R p) (-x) = -(frobenius R p) x

theorem frobenius_sub (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R p] (x y : R) :
(frobenius R p) (x - y) = (frobenius R p) x - (frobenius R p) y

theorem frobenius_nat_cast (R : Type u) [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R p] (n : ) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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