HepLean 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.

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

source
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
source
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
source
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.

source
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.

source
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.

source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
instance Prod.charZero_of_left (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero R] :
CharZero (R × S)
Equations
  • ⋯ = ⋯
source
instance Prod.charZero_of_right (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero S] :
CharZero (R × S)
Equations
  • ⋯ = ⋯
source
instance ULift.charP (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] :
CharP (ULift.{u_2, u_1} R) p
Equations
  • ⋯ = ⋯
source
instance MulOpposite.charP (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] :
CharP Rᵐᵒᵖ p
Equations
  • ⋯ = ⋯
source
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.

source
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
source
instance Fin.charP (n : ℕ) [NeZero n] :
CharP (Fin n) n
Equations
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯