algebra.char_p.basic - mathlib3 docs

@[protected]

theorem commute.add_pow_prime_pow_eq {R : Type u_1} [semiring R] {p : ℕ} {x y : R} (hp : nat.prime p) (h : commute x y) (n : ℕ) :

(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * (finset.Ioo 0 (p ^ n)).sum (λ (k : ℕ), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p))

source

@[protected]

theorem commute.add_pow_prime_eq {R : Type u_1} [semiring R] {p : ℕ} {x y : R} (hp : nat.prime p) (h : commute x y) :

(x + y) ^ p = x ^ p + y ^ p + ↑p * (finset.Ioo 0 p).sum (λ (k : ℕ), x ^ k * y ^ (p - k) * ↑(p.choose k / p))

source

@[protected]

theorem commute.exists_add_pow_prime_pow_eq {R : Type u_1} [semiring R] {p : ℕ} {x y : R} (hp : nat.prime p) (h : commute x y) (n : ℕ) :

∃ (r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r

source

@[protected]

theorem commute.exists_add_pow_prime_eq {R : Type u_1} [semiring R] {p : ℕ} {x y : R} (hp : nat.prime p) (h : commute x y) :

∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + ↑p * r

source

theorem add_pow_prime_pow_eq {R : Type u_1} [comm_semiring R] {p : ℕ} (hp : nat.prime p) (x y : R) (n : ℕ) :

(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * (finset.Ioo 0 (p ^ n)).sum (λ (k : ℕ), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p))

source

theorem add_pow_prime_eq {R : Type u_1} [comm_semiring R] {p : ℕ} (hp : nat.prime p) (x y : R) :

(x + y) ^ p = x ^ p + y ^ p + ↑p * (finset.Ioo 0 p).sum (λ (k : ℕ), x ^ k * y ^ (p - k) * ↑(p.choose k / p))

source

theorem exists_add_pow_prime_pow_eq {R : Type u_1} [comm_semiring R] {p : ℕ} (hp : nat.prime p) (x y : R) (n : ℕ) :

∃ (r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r

source

theorem exists_add_pow_prime_eq {R : Type u_1} [comm_semiring R] {p : ℕ} (hp : nat.prime p) (x y : R) :

∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + ↑p * r

source

theorem char_p_iff (R : Type u_1) [add_monoid_with_one R] (p : ℕ) :

char_p R p ↔ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x

source

@[class]

structure char_p (R : Type u_1) [add_monoid_with_one R] (p : ℕ) :

Prop

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, 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

source

@[simp]

theorem char_p.cast_eq_zero (R : Type u_1) [add_monoid_with_one R] (p : ℕ) [char_p R p] :

↑p = 0

source

@[simp]

theorem char_p.cast_card_eq_zero (R : Type u_1) [add_group_with_one R] [fintype R] :

↑(fintype.card R) = 0

source

theorem char_p.add_order_of_one (R : Type u_1) [semiring R] :

char_p R (add_order_of 1)

source

theorem char_p.int_cast_eq_zero_iff (R : Type u_1) [add_group_with_one R] (p : ℕ) [char_p R p] (a : ℤ) :

↑a = 0 ↔ ↑p ∣ a

source

theorem char_p.int_cast_eq_int_cast (R : Type u_1) [add_group_with_one R] (p : ℕ) [char_p R p] {a b : ℤ} :

↑a = ↑b ↔ a ≡ b [ZMOD ↑p]

source

theorem char_p.nat_cast_eq_nat_cast (R : Type u_1) [add_group_with_one R] (p : ℕ) [char_p R p] {a b : ℕ} :

↑a = ↑b ↔ a ≡ b [MOD p]

source

theorem char_p.eq (R : Type u_1) [add_monoid_with_one R] {p q : ℕ} (c1 : char_p R p) (c2 : char_p R q) :

p = q

source

@[protected, instance]

def char_p.of_char_zero (R : Type u_1) [add_monoid_with_one R] [char_zero R] :

char_p R 0

source

theorem char_p.exists (R : Type u_1) [non_assoc_semiring R] :

∃ (p : ℕ), char_p R p

source

theorem char_p.exists_unique (R : Type u_1) [non_assoc_semiring R] :

∃! (p : ℕ), char_p R p

source

theorem char_p.congr {R : Type u} [add_monoid_with_one R] {p : ℕ} (q : ℕ) [hq : char_p R q] (h : q = p) :

char_p R p

source

noncomputable def ring_char (R : Type u_1) [non_assoc_semiring R] :

ℕ

Noncomputable function that outputs the unique characteristic of a semiring.

Equations

ring_char R = classical.some _

Instances for ring_char

ring_char.char_p

source

theorem ring_char.spec (R : Type u_1) [non_assoc_semiring R] (x : ℕ) :

↑x = 0 ↔ ring_char R ∣ x

source

theorem ring_char.eq (R : Type u_1) [non_assoc_semiring R] (p : ℕ) [C : char_p R p] :

ring_char R = p

source

@[protected, instance]

def ring_char.char_p (R : Type u_1) [non_assoc_semiring R] :

char_p R (ring_char R)

source

theorem ring_char.of_eq {R : Type u_1} [non_assoc_semiring R] {p : ℕ} (h : ring_char R = p) :

char_p R p

source

theorem ring_char.eq_iff {R : Type u_1} [non_assoc_semiring R] {p : ℕ} :

ring_char R = p ↔ char_p R p

source

theorem ring_char.dvd {R : Type u_1} [non_assoc_semiring R] {x : ℕ} (hx : ↑x = 0) :

ring_char R ∣ x

source

@[simp]

theorem ring_char.eq_zero {R : Type u_1} [non_assoc_semiring R] [char_zero R] :

ring_char R = 0

source

@[simp]

theorem ring_char.nat.cast_ring_char {R : Type u_1} [non_assoc_semiring R] :

↑(ring_char R) = 0

source

theorem add_pow_char_of_commute (R : Type u_1) [semiring R] {p : ℕ} [hp : fact (nat.prime p)] [char_p R p] (x y : R) (h : commute x y) :

(x + y) ^ p = x ^ p + y ^ p

source

theorem add_pow_char_pow_of_commute (R : Type u_1) [semiring R] {p n : ℕ} [hp : fact (nat.prime p)] [char_p R p] (x y : R) (h : commute x y) :

(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

source

theorem sub_pow_char_of_commute (R : Type u_1) [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

source

theorem sub_pow_char_pow_of_commute (R : Type u_1) [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

source

theorem add_pow_char (R : Type u_1) [comm_semiring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] (x y : R) :

(x + y) ^ p = x ^ p + y ^ p

source

theorem add_pow_char_pow (R : Type u_1) [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

source

theorem sub_pow_char (R : Type u_1) [comm_ring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] (x y : R) :

(x - y) ^ p = x ^ p - y ^ p

source

theorem sub_pow_char_pow (R : Type u_1) [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

source

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

-1 ≠ 1

source

theorem char_p.neg_one_pow_char (R : Type u_1) [comm_ring R] (p : ℕ) [char_p R p] [fact (nat.prime p)] :

(-1) ^ p = -1

source

theorem char_p.neg_one_pow_char_pow (R : Type u_1) [comm_ring R] (p n : ℕ) [char_p R p] [fact (nat.prime p)] :

(-1) ^ p ^ n = -1

source

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

char_p K p ↔ char_p L p

source

def frobenius (R : Type u_1) [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :

R →+* R

The frobenius map that sends x to x^p

Equations

frobenius R p = {to_fun := λ (x : R), x ^ p, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem frobenius_def {R : Type u_1} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (x : R) :

⇑(frobenius R p) x = x ^ p

source

theorem iterate_frobenius {R : Type u_1} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (x : R) (n : ℕ) :

⇑(frobenius R p)^[n] x = x ^ p ^ n

source

theorem frobenius_mul {R : Type u_1} [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

source

theorem frobenius_one {R : Type u_1} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :

⇑(frobenius R p) 1 = 1

source

theorem monoid_hom.map_frobenius {R : Type u_1} [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)

source

theorem ring_hom.map_frobenius {R : Type u_1} [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)

source

theorem monoid_hom.map_iterate_frobenius {R : Type u_1} [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)

source

theorem ring_hom.map_iterate_frobenius {R : Type u_1} [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)

source

theorem monoid_hom.iterate_map_frobenius {R : Type u_1} [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)

source

theorem ring_hom.iterate_map_frobenius {R : Type u_1} [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)

source

theorem frobenius_zero (R : Type u_1) [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :

⇑(frobenius R p) 0 = 0

source

theorem frobenius_add (R : Type u_1) [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

source

theorem frobenius_nat_cast (R : Type u_1) [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (n : ℕ) :

⇑(frobenius R p) ↑n = ↑n

source

theorem list_sum_pow_char {R : Type u_1} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (l : list R) :

l.sum ^ p = (list.map (λ (_x : R), _x ^ p) l).sum

source

theorem multiset_sum_pow_char {R : Type u_1} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (s : multiset R) :

s.sum ^ p = (multiset.map (λ (_x : R), _x ^ p) s).sum

source

theorem sum_pow_char {R : Type u_1} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] {ι : Type u_2} (s : finset ι) (f : ι → R) :

s.sum (λ (i : ι), f i) ^ p = s.sum (λ (i : ι), f i ^ p)

source

theorem frobenius_neg (R : Type u_1) [comm_ring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (x : R) :

⇑(frobenius R p) (-x) = -⇑(frobenius R p) x

source

theorem frobenius_sub (R : Type u_1) [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

source

theorem frobenius_inj (R : Type u_1) [comm_ring R] [is_reduced R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :

function.injective ⇑(frobenius R p)

source

theorem is_square_of_char_two' {R : Type u_1} [finite R] [comm_ring R] [is_reduced R] [char_p R 2] (a : R) :

is_square a

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

source

theorem char_p.char_p_to_char_zero (R : Type u_1) [add_group_with_one R] [char_p R 0] :

char_zero R

source

theorem char_p.cast_eq_mod (R : Type u_1) [non_assoc_ring R] (p : ℕ) [char_p R p] (k : ℕ) :

↑k = ↑(k % p)

source

theorem char_p.char_ne_zero_of_finite (R : Type u_1) [non_assoc_ring R] (p : ℕ) [char_p R p] [finite R] :

p ≠ 0

The characteristic of a finite ring cannot be zero.

source

theorem char_p.ring_char_ne_zero_of_finite (R : Type u_1) [non_assoc_ring R] [finite R] :

ring_char R ≠ 0

source

@[simp]

theorem char_p.pow_prime_pow_mul_eq_one_iff {R : Type u_1} [comm_ring R] [is_reduced R] (p k m : ℕ) [fact (nat.prime p)] [char_p R p] (x : R) :

x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

source

theorem char_p.char_ne_one (R : Type u_1) [non_assoc_semiring R] [nontrivial R] (p : ℕ) [hc : char_p R p] :

p ≠ 1

source

theorem char_p.char_is_prime_of_two_le (R : Type u_1) [non_assoc_semiring R] [no_zero_divisors R] (p : ℕ) [hc : char_p R p] (hp : 2 ≤ p) :

nat.prime p

source

theorem char_p.char_is_prime_or_zero (R : Type u_1) [non_assoc_semiring R] [no_zero_divisors R] [nontrivial R] (p : ℕ) [hc : char_p R p] :

nat.prime p ∨ p = 0

source

theorem char_p.char_is_prime_of_pos (R : Type u_1) [non_assoc_semiring R] [no_zero_divisors R] [nontrivial R] (p : ℕ) [ne_zero p] [char_p R p] :

fact (nat.prime p)

source

theorem char_p.char_is_prime (R : Type u_1) [ring R] [no_zero_divisors R] [nontrivial R] [finite R] (p : ℕ) [char_p R p] :

nat.prime p

source

@[protected, instance]

def char_p.subsingleton {R : Type u_1} [non_assoc_semiring R] [char_p R 1] :

subsingleton R

source

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

false

source

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

ring_char R ≠ 1

source

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

nontrivial R

source

theorem char_p.ring_char_of_prime_eq_zero {R : Type u_1} [non_assoc_semiring R] [nontrivial R] {p : ℕ} (hprime : nat.prime p) (hp0 : ↑p = 0) :

ring_char R = p

source

@[protected]

theorem ring.two_ne_zero {R : Type u_1} [non_assoc_semiring R] [nontrivial R] (hR : ring_char R ≠ 2) :

2 ≠ 0

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

source

theorem ring.neg_one_ne_one_of_char_ne_two {R : Type u_1} [non_assoc_ring R] [nontrivial R] (hR : ring_char R ≠ 2) :

-1 ≠ 1

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

source

theorem ring.eq_self_iff_eq_zero_of_char_ne_two {R : Type u_1} [non_assoc_ring R] [nontrivial R] [no_zero_divisors R] (hR : ring_char R ≠ 2) {a : R} :

-a = a ↔ a = 0

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

source

theorem char_p_of_ne_zero (R : Type u_1) [non_assoc_ring R] [fintype R] (n : ℕ) (hn : fintype.card R = n) (hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0) :

char_p R n

source

theorem char_p_of_prime_pow_injective (R : Type u_1) [ring R] [fintype R] (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) (hn : fintype.card R = p ^ n) (hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n) :

char_p R (p ^ n)

source

@[protected, instance]

def nat.lcm.char_p (R : Type u_1) (S : Type v) [add_monoid_with_one R] [add_monoid_with_one S] (p q : ℕ) [char_p R p] [char_p S 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.

source

@[protected, instance]

def prod.char_p (R : Type u_1) (S : Type v) [add_monoid_with_one R] [add_monoid_with_one S] (p : ℕ) [char_p R p] [char_p S 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

source

@[protected, instance]

def ulift.char_p (R : Type u_1) [add_monoid_with_one R] (p : ℕ) [char_p R p] :

char_p (ulift R) p

source

@[protected, instance]

def mul_opposite.char_p (R : Type u_1) [add_monoid_with_one R] (p : ℕ) [char_p R p] :

char_p Rᵐᵒᵖ p

source

theorem int.cast_inj_on_of_ring_char_ne_two {R : Type u_1} [non_assoc_ring R] [nontrivial R] (hR : ring_char R ≠ 2) :

set.inj_on coe {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.

source

theorem ne_zero.of_not_dvd (R : Type u_1) [add_monoid_with_one R] {n p : ℕ} [char_p R p] (h : ¬p ∣ n) :

ne_zero ↑n

source

theorem ne_zero.not_char_dvd (R : Type u_1) [add_monoid_with_one R] (p : ℕ) [char_p R p] (k : ℕ) [h : ne_zero ↑k] :

¬p ∣ k

mathlib3 documentation

Characteristic of semirings #