mathlib documentation

algebra.char_p.basic

Characteristic of semirings #

@[class]
structure char_p (R : Type u) [add_monoid R] [has_one R] (p : ) :
Prop

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

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

Noncomputable function that outputs the unique characteristic of a semiring.

Equations
theorem ring_char.spec (R : Type u) [semiring R] (x : ) :
theorem ring_char.eq (R : Type u) [semiring R] {p : } (C : char_p R p) :
@[instance]
def ring_char.char_p (R : Type u) [semiring R] :
theorem ring_char.of_eq {R : Type u} [semiring R] {p : } (h : ring_char R = p) :
char_p R p
theorem ring_char.eq_iff {R : Type u} [semiring R] {p : } :
theorem ring_char.dvd {R : Type u} [semiring R] {x : } (hx : x = 0) :
@[simp]
theorem ring_char.eq_zero {R : Type u} [semiring R] [char_zero R] :
theorem add_pow_char_of_commute (R : Type u) [semiring R] {p : } [fact (nat.prime p)] [char_p R p] (x y : R) (h : commute x 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)] [char_p R p] {n : } (x 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) [ring R] {p : } [fact (nat.prime p)] [char_p R p] (x y : R) (h : 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) (h : commute x y) :
(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
theorem add_pow_char (R : Type u) [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] (x y : R) :
(x + y) ^ p = x ^ p + y ^ p
theorem add_pow_char_pow (R : Type u) [comm_semiring 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 (R : Type u) [comm_ring R] {p : } [fact (nat.prime p)] [char_p R 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)] [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) [ring R] (p : ) [char_p R p] (a b : ) :
theorem char_p.neg_one_ne_one (R : Type u) [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_semiring 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_semiring 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_semiring 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_semiring 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_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] :
(frobenius R p) 1 = 1
theorem monoid_hom.map_frobenius {R : Type u} [comm_semiring R] {S : Type v} [comm_semiring 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_semiring R] {S : Type v} [comm_semiring 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_semiring R] {S : Type v} [comm_semiring 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_semiring R] {S : Type v} [comm_semiring 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_semiring 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_semiring 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_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] :
(frobenius R p) 0 = 0
theorem frobenius_add (R : Type u) [comm_semiring 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_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (n : ) :
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_inj (R : Type u) [comm_ring R] [no_zero_divisors R] (p : ) [fact (nat.prime p)] [char_p R p] :
theorem char_p.char_p_to_char_zero (R : Type u) [ring R] [char_p R 0] :
theorem char_p.cast_eq_mod (R : Type u) [ring R] (p : ) [char_p R p] (k : ) :
k = (k % p)
theorem char_p.char_ne_zero_of_fintype (R : Type u) [ring R] (p : ) [hc : char_p R p] [fintype R] :
p 0
theorem char_p.char_ne_one (R : Type u) [semiring R] [nontrivial R] (p : ) [hc : char_p R p] :
p 1
theorem char_p.char_is_prime_of_two_le (R : Type u) [semiring R] [no_zero_divisors R] (p : ) [hc : char_p R p] (hp : 2 p) :
theorem char_p.char_is_prime_or_zero (R : Type u) [semiring R] [no_zero_divisors R] [nontrivial R] (p : ) [hc : char_p R p] :
theorem char_p.char_is_prime_of_pos (R : Type u) [semiring R] [no_zero_divisors R] [nontrivial R] (p : ) [h : fact (0 < p)] [char_p R p] :
theorem char_p.char_is_prime (R : Type u) [ring R] [no_zero_divisors R] [nontrivial R] [fintype R] (p : ) [char_p R p] :
@[instance]
def char_p.subsingleton {R : Type u} [semiring R] [char_p R 1] :
theorem char_p.ring_char_ne_one {R : Type u} [semiring R] [nontrivial R] :
theorem char_p.nontrivial_of_char_ne_one {R : Type u} [semiring R] {v : } (hv : v 1) [hr : char_p R v] :
theorem char_p_of_ne_zero (R : Type u) [comm_ring R] [fintype R] (n : ) (hn : fintype.card R = n) (hR : ∀ (i : ), i < ni = 0i = 0) :
char_p R n
theorem char_p_of_prime_pow_injective (R : Type u) [comm_ring R] [fintype R] (p : ) [hp : fact (nat.prime p)] (n : ) (hn : fintype.card R = p ^ n) (hR : ∀ (i : ), i np ^ i = 0i = n) :
char_p R (p ^ n)