Documentation

Mathlib.Algebra.CharP.Basic

Characteristic of semirings #

This file collects some fundamental results on the characteristic of rings that don't need the extra imports of CharP/Lemmas.lean.

As such, we can probably reorganize and find a better home for most of these lemmas.

theorem CharP.intCast_injOn_Ico (R : Type u_1) [AddGroupWithOne R] (p : ) [CharP R p] [IsRightCancelAdd R] :
Set.InjOn Int.cast (Set.Ico 0 p)
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_ne_zero_of_ne_of_prime (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] {p : } {q : } [CharP R p] (hq : Nat.Prime q) (hneq : p q) :
q 0

If a ring R is of characteristic p, then for any prime number q different from p, it is not zero in R.

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.

instance Nat.lcm.charP (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] (p : ) (q : ) [CharP R p] [CharP S q] :
CharP (R × S) (p.lcm 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 u_2) [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 u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero R] :
CharZero (R × S)
Equations
  • =
instance Prod.charZero_of_right (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero S] :
CharZero (R × S)
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.

instance Fin.charP (n : ) [NeZero n] :
CharP (Fin n) n

The characteristic of F_p is p.

Equations
  • =
instance instExpCharProd (R : Type u_1) [AddMonoidWithOne R] (S : Type u_2) [Semiring S] (p : ) [ExpChar R p] [ExpChar S p] :
ExpChar (R × S) p
Equations
  • =