Documentation

Mathlib.Algebra.CharP.Basic

Characteristic of semirings #

theorem Commute.add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : } {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * Finset.sum (Finset.Ioo 0 (p ^ n)) fun (k : ) => x ^ k * y ^ (p ^ n - k) * (Nat.choose (p ^ n) k / p)
theorem Commute.add_pow_prime_eq {R : Type u_1} [Semiring R] {p : } {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) :
(x + y) ^ p = x ^ p + y ^ p + p * Finset.sum (Finset.Ioo 0 p) fun (k : ) => x ^ k * y ^ (p - k) * (Nat.choose p k / p)
theorem Commute.exists_add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : } {x : R} {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
theorem Commute.exists_add_pow_prime_eq {R : Type u_1} [Semiring R] {p : } {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) :
∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + p * r
theorem add_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : } (hp : Nat.Prime p) (x : R) (y : R) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * Finset.sum (Finset.Ioo 0 (p ^ n)) fun (k : ) => x ^ k * y ^ (p ^ n - k) * (Nat.choose (p ^ n) k / p)
theorem add_pow_prime_eq {R : Type u_1} [CommSemiring R] {p : } (hp : Nat.Prime p) (x : R) (y : R) :
(x + y) ^ p = x ^ p + y ^ p + p * Finset.sum (Finset.Ioo 0 p) fun (k : ) => x ^ k * y ^ (p - k) * (Nat.choose p k / p)
theorem exists_add_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : } (hp : Nat.Prime p) (x : R) (y : R) (n : ) :
∃ (r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r
theorem exists_add_pow_prime_eq {R : Type u_1} [CommSemiring R] {p : } (hp : Nat.Prime p) (x : R) (y : R) :
∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + p * r
theorem charP_iff (R : Type u_1) [AddMonoidWithOne R] (p : ) :
CharP R p ∀ (x : ), x = 0 p x
class CharP (R : Type u_1) [AddMonoidWithOne R] (p : ) :

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

Warning: for a semiring R, CharP R 0 and CharZero R need not coincide.

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

For instance, endowing {0, 1} with addition given by max (i.e. 1 is absorbing), shows that CharZero {0, 1} does not hold and yet CharP {0, 1} 0 does. This example is formalized in Counterexamples/CharPZeroNeCharZero.lean.

  • cast_eq_zero_iff' : ∀ (x : ), x = 0 p x
Instances
    theorem CharP.cast_eq_zero_iff (R : Type u) [AddMonoidWithOne R] (p : ) [CharP R p] (x : ) :
    x = 0 p x
    @[simp]
    theorem CharP.cast_eq_zero (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] :
    p = 0
    @[simp]
    theorem CharP.int_cast_eq_zero_iff (R : Type u_1) [AddGroupWithOne R] (p : ) [CharP R p] (a : ) :
    a = 0 p a
    theorem CharP.intCast_eq_intCast (R : Type u_1) [AddGroupWithOne R] (p : ) [CharP R p] {a : } {b : } :
    a = b a b [ZMOD p]
    theorem CharP.natCast_eq_natCast' (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] {a : } {b : } (h : a b [MOD p]) :
    a = b
    theorem CharP.natCast_eq_natCast (R : Type u_1) [AddMonoidWithOne R] [IsRightCancelAdd R] (p : ) [CharP R p] {a : } {b : } :
    a = b a b [MOD p]
    theorem CharP.intCast_eq_intCast_mod (R : Type u_1) [AddGroupWithOne R] (p : ) [CharP R p] {a : } :
    a = (a % p)
    theorem CharP.natCast_eq_natCast_mod (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] {a : } :
    a = (a % p)
    theorem CharP.eq (R : Type u_1) [AddMonoidWithOne R] {p : } {q : } (_c1 : CharP R p) (_c2 : CharP R q) :
    p = q
    instance CharP.ofCharZero (R : Type u_1) [AddMonoidWithOne R] [CharZero R] :
    CharP R 0
    Equations
    • =
    theorem CharP.exists (R : Type u_1) [NonAssocSemiring R] :
    ∃ (p : ), CharP R p
    theorem CharP.exists_unique (R : Type u_1) [NonAssocSemiring R] :
    ∃! (p : ), CharP R p
    theorem CharP.congr {R : Type u} [AddMonoidWithOne R] {p : } (q : ) [hq : CharP R q] (h : q = p) :
    CharP R p
    noncomputable def ringChar (R : Type u_1) [NonAssocSemiring R] :

    Noncomputable function that outputs the unique characteristic of a semiring.

    Equations
    Instances For
      theorem ringChar.spec (R : Type u_1) [NonAssocSemiring R] (x : ) :
      x = 0 ringChar R x
      theorem ringChar.eq (R : Type u_1) [NonAssocSemiring R] (p : ) [C : CharP R p] :
      instance ringChar.charP (R : Type u_1) [NonAssocSemiring R] :
      Equations
      • =
      theorem ringChar.of_eq {R : Type u_1} [NonAssocSemiring R] {p : } (h : ringChar R = p) :
      CharP R p
      theorem ringChar.eq_iff {R : Type u_1} [NonAssocSemiring R] {p : } :
      theorem ringChar.dvd {R : Type u_1} [NonAssocSemiring R] {x : } (hx : x = 0) :
      @[simp]
      theorem ringChar.eq_zero {R : Type u_1} [NonAssocSemiring R] [CharZero R] :
      theorem add_pow_char_of_commute (R : Type u_1) [Semiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) (h : Commute x y) :
      (x + y) ^ p = x ^ p + y ^ p
      theorem add_pow_char_pow_of_commute (R : Type u_1) [Semiring R] {p : } {n : } [hp : Fact (Nat.Prime p)] [CharP R p] (x : R) (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_1) [Ring R] {p : } [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) (h : Commute x y) :
      (x - y) ^ p = x ^ p - y ^ p
      theorem sub_pow_char_pow_of_commute (R : Type u_1) [Ring R] {p : } [Fact (Nat.Prime p)] [CharP R p] {n : } (x : R) (y : R) (h : Commute x y) :
      (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
      theorem add_pow_char (R : Type u_1) [CommSemiring R] {p : } [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) :
      (x + y) ^ p = x ^ p + y ^ p
      theorem add_pow_char_pow (R : Type u_1) [CommSemiring R] {p : } [Fact (Nat.Prime p)] [CharP R p] {n : } (x : R) (y : R) :
      (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
      theorem sub_pow_char (R : Type u_1) [CommRing R] {p : } [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) :
      (x - y) ^ p = x ^ p - y ^ p
      theorem sub_pow_char_pow (R : Type u_1) [CommRing R] {p : } [Fact (Nat.Prime p)] [CharP R p] {n : } (x : R) (y : R) :
      (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
      theorem CharP.neg_one_ne_one (R : Type u_1) [Ring R] (p : ) [CharP R p] [Fact (2 < p)] :
      -1 1
      theorem CharP.neg_one_pow_char (R : Type u_1) [Ring R] (p : ) [CharP R p] [Fact (Nat.Prime p)] :
      (-1) ^ p = -1
      theorem CharP.neg_one_pow_char_pow (R : Type u_1) [Ring R] (p : ) (n : ) [CharP R p] [Fact (Nat.Prime p)] :
      (-1) ^ p ^ n = -1
      theorem RingHom.charP_iff_charP {K : Type u_2} {L : Type u_3} [DivisionRing K] [Semiring L] [Nontrivial L] (f : K →+* L) (p : ) :
      CharP K p CharP L p
      theorem CharP.cast_eq_mod (R : Type u_1) [NonAssocRing R] (p : ) [CharP R p] (k : ) :
      k = (k % p)
      theorem CharP.char_ne_zero_of_finite (R : Type u_1) [NonAssocRing R] (p : ) [CharP R p] [Finite R] :
      p 0

      The characteristic of a finite ring cannot be zero.

      theorem CharP.char_ne_one (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] (p : ) [hc : CharP R p] :
      p 1
      theorem CharP.char_is_prime_of_two_le (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] (p : ) [hc : CharP R p] (hp : 2 p) :
      theorem CharP.exists' (R : Type u_2) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] :
      CharZero R ∃ (p : ), Fact (Nat.Prime p) CharP R p
      theorem CharP.char_is_prime (R : Type u_1) [Ring R] [NoZeroDivisors R] [Nontrivial R] [Finite R] (p : ) [CharP R p] :
      Equations
      • =
      theorem CharP.nontrivial_of_char_ne_one {R : Type u_1} [NonAssocSemiring R] {v : } (hv : v 1) [hr : CharP R v] :
      theorem CharP.ringChar_of_prime_eq_zero {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] {p : } (hprime : Nat.Prime p) (hp0 : p = 0) :
      theorem CharP.charP_iff_prime_eq_zero {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] {p : } (hp : Nat.Prime p) :
      CharP R p p = 0
      theorem Ring.two_ne_zero {R : Type u_2} [NonAssocSemiring R] [Nontrivial R] (hR : ringChar R 2) :
      2 0

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

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

      theorem Ring.eq_self_iff_eq_zero_of_char_ne_two {R : Type u_2} [NonAssocRing R] [Nontrivial R] [NoZeroDivisors R] (hR : ringChar R 2) {a : R} :
      -a = a a = 0

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

      theorem charP_of_ne_zero (R : Type u_1) [NonAssocRing R] [Fintype R] (n : ) (hn : Fintype.card R = n) (hR : i < n, i = 0i = 0) :
      CharP R n
      theorem charP_of_prime_pow_injective (R : Type u_2) [Ring R] [Fintype R] (p : ) [hp : Fact (Nat.Prime p)] (n : ) (hn : Fintype.card R = p ^ n) (hR : in, p ^ i = 0i = n) :
      CharP R (p ^ n)
      instance Nat.lcm.charP (R : Type u_1) (S : Type v) [AddMonoidWithOne R] [AddMonoidWithOne S] (p : ) (q : ) [CharP R p] [CharP S q] :
      CharP (R × S) (Nat.lcm p q)

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

      Equations
      • =
      instance Prod.charP (R : Type u_1) (S : Type v) [AddMonoidWithOne R] [AddMonoidWithOne S] (p : ) [CharP R p] [CharP S p] :
      CharP (R × S) p

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

      Equations
      • =
      instance Prod.charZero_of_left (R : Type u_1) (S : Type v) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero R] :
      CharZero (R × S)
      Equations
      • =
      Equations
      • =
      instance ULift.charP (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] :
      Equations
      • =
      instance MulOpposite.charP (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] :
      Equations
      • =
      theorem Int.cast_injOn_of_ringChar_ne_two {R : Type u_2} [NonAssocRing R] [Nontrivial R] (hR : ringChar R 2) :
      Set.InjOn Int.cast {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 NeZero.of_not_dvd (R : Type u_1) [AddMonoidWithOne R] {n : } {p : } [CharP R p] (h : ¬p n) :
      NeZero n
      theorem NeZero.not_char_dvd (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] (k : ) [h : NeZero k] :
      ¬p k
      instance Fin.charP (n : ) :
      CharP (Fin (n + 1)) (n + 1)
      Equations
      • =