Documentation

Mathlib.Algebra.CharP.Defs

Characteristic of semirings #

Main definitions #

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_iff (R : Type u_1) [AddMonoidWithOne R] (p : ) :
    CharP R p ∀ (x : ), x = 0 p x
    theorem CharP.cast_eq_zero_iff (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] (a : ) :
    a = 0 p a
    theorem CharP.congr {R : Type u_1} [AddMonoidWithOne R] (p : ) [CharP R p] {q : } (h : p = q) :
    CharP R q
    theorem CharP.natCast_eq_natCast' (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] {a b : } (h : a b [MOD p]) :
    a = b
    @[simp]
    theorem CharP.cast_eq_zero (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] :
    p = 0
    theorem CharP.ofNat_eq_zero (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] [p.AtLeastTwo] :
    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 : } (_hp : CharP R p) (_hq : CharP R q) :
    p = q
    theorem CharP.natCast_eq_natCast (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] {a b : } [IsRightCancelAdd R] :
    a = b a b [MOD p]
    theorem CharP.intCast_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.intCast_eq_intCast_mod (R : Type u_1) [AddGroupWithOne R] (p : ) [CharP R p] {a : } :
    a = (a % p)
    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
    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] :
      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 CharP.neg_one_ne_one (R : Type u_1) [Ring R] (p : ) [CharP R p] [Fact (2 < p)] :
      -1 1
      theorem CharP.cast_eq_mod (R : Type u_1) [NonAssocRing R] (p : ) [CharP R p] (k : ) :
      k = (k % p)
      theorem CharP.char_ne_one (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] (p : ) [hc : CharP R p] :
      p 1
      theorem CharP.char_prime_of_ne_zero (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] {p : } [CharP R p] (hp : p 0) :

      The characteristic is prime if it is non-zero.

      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.nontrivial_of_char_ne_one {R : Type u_1} [NonAssocSemiring R] {v : } (hv : v 1) [hr : CharP R v] :
      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

      Exponential characteristic #

      This section defines the exponential characteristic, which is defined to be 1 for a ring with characteristic 0 and the same as the ordinary characteristic, if the ordinary characteristic is prime. This concept is useful to simplify some theorem statements. This file establishes a few basic results relating it to the (ordinary characteristic). The definition is stated for a semiring, but the actual results are for nontrivial rings (as far as exponential characteristic one is concerned), respectively a ring without zero-divisors (for prime characteristic).

      class inductive ExpChar (R : Type u_1) [AddMonoidWithOne R] :
      Prop

      The definition of the exponential characteristic of a semiring.

      Instances
        instance expChar_prime (R : Type u_1) [AddMonoidWithOne R] (p : ) [CharP R p] [Fact (Nat.Prime p)] :
        instance expChar_one (R : Type u_1) [AddMonoidWithOne R] [CharZero R] :
        theorem expChar_ne_zero (R : Type u_1) [AddMonoidWithOne R] (p : ) [hR : ExpChar R p] :
        p 0
        theorem ExpChar.eq {R : Type u_1} [AddMonoidWithOne R] {p q : } (hp : ExpChar R p) (hq : ExpChar R q) :
        p = q

        The exponential characteristic is unique.

        theorem ExpChar.congr (R : Type u_1) [AddMonoidWithOne R] {p : } (q : ) [hq : ExpChar R q] (h : q = p) :
        theorem expChar_one_of_char_zero (R : Type u_1) [AddMonoidWithOne R] (q : ) [hp : CharP R 0] [hq : ExpChar R q] :
        q = 1

        The exponential characteristic is one if the characteristic is zero.

        theorem char_eq_expChar_iff (R : Type u_1) [AddMonoidWithOne R] (p q : ) [hp : CharP R p] [hq : ExpChar R q] :

        The characteristic equals the exponential characteristic iff the former is prime.

        theorem expChar_is_prime_or_one (R : Type u_1) [AddMonoidWithOne R] (q : ) [hq : ExpChar R q] :

        The exponential characteristic is a prime number or one. See also CharP.char_is_prime_or_zero.

        theorem expChar_pos (R : Type u_1) [AddMonoidWithOne R] (q : ) [ExpChar R q] :
        0 < q

        The exponential characteristic is positive.

        theorem expChar_pow_pos (R : Type u_1) [AddMonoidWithOne R] (q : ) [ExpChar R q] (n : ) :
        0 < q ^ n

        Any power of the exponential characteristic is positive.

        noncomputable def ringExpChar (R : Type u_1) [NonAssocSemiring R] :

        Noncomputable function that outputs the unique exponential characteristic of a semiring.

        Equations
        Instances For
          theorem ringExpChar.eq (R : Type u_1) [NonAssocSemiring R] (q : ) [h : ExpChar R q] :
          @[simp]
          theorem char_zero_of_expChar_one (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] (p : ) [hp : CharP R p] [hq : ExpChar R 1] :
          p = 0

          The exponential characteristic is one if the characteristic is zero.

          The characteristic is zero if the exponential characteristic is one.

          theorem expChar_one_iff_char_zero (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] (p q : ) [CharP R p] [ExpChar R q] :
          q = 1 p = 0

          The exponential characteristic is one iff the characteristic is zero.

          theorem ExpChar.exists (R : Type u_1) [Ring R] [IsDomain R] :
          ∃ (q : ), ExpChar R q
          theorem ExpChar.exists_unique (R : Type u_1) [Ring R] [IsDomain R] :
          ∃! q : , ExpChar R q
          theorem ringExpChar.of_eq {R : Type u_1} [Ring R] [IsDomain R] {q : } (h : ringExpChar R = q) :
          theorem ringExpChar.eq_iff {R : Type u_1} [Ring R] [IsDomain R] {q : } :