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.natCast_injOn_Iio (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] [IsRightCancelAdd R] : Set.InjOn Nat.cast (Set.Iio p)

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) : ringChar R = p

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.

theorem Ring.neg_one_ne_one_of_char_ne_two {R : Type u_2} [NonAssocRing R] [Nontrivial R] (hR : ringChar R ≠ 2) : -1 ≠ 1

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.

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

instance Prod.charZero_of_left (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero R] : CharZero (R × S)

instance Prod.charZero_of_right (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero S] : CharZero (R × S)

instance ULift.charP (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift.{u_2, u_1} R) p

instance MulOpposite.charP (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP Rᵐᵒᵖ p

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 CharZero.charZero_iff_forall_prime_ne_zero (R : Type u_1) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0

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

The characteristic of F_p is p.

Stacks Tag 09FS (First part. We don't require p to be a prime in mathlib.)

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