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 Mathlib/Algebra/CharP/Lemmas.lean.

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

source
๐Ÿ“ coverage
theorem CharP.natCast_eq_natCast' (R : Type u_1) [AddMonoidWithOne R] (p : โ„•) [CharP R p] {a b : โ„•} (h : a โ‰ก b [MOD p]) :
โ†‘a = โ†‘b
source
๐Ÿ“ coverage
theorem CharP.natCast_eq_natCast_mod (R : Type u_1) [AddMonoidWithOne R] (p : โ„•) [CharP R p] (a : โ„•) :
โ†‘a = โ†‘(a % p)
source
๐Ÿ“ coverage
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]
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
theorem CharP.intCast_eq_intCast (R : Type u_1) [AddGroupWithOne R] (p : โ„•) [CharP R p] {a b : โ„ค} :
โ†‘a = โ†‘b โ†” a โ‰ก b [ZMOD โ†‘p]
source
๐Ÿ“ coverage
theorem CharP.intCast_eq_intCast_mod (R : Type u_1) [AddGroupWithOne R] (p : โ„•) [CharP R p] {a : โ„ค} :
โ†‘a = โ†‘(a % โ†‘p)
source
๐Ÿ“ coverage
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 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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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.

source
๐Ÿ“ coverage
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

source
๐Ÿ“ coverage
instance Prod.charZero_of_left (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero R] :
CharZero (R ร— S)
source
๐Ÿ“ coverage
instance Prod.charZero_of_right (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero S] :
CharZero (R ร— S)
source
๐Ÿ“ coverage
instance ULift.charP (R : Type u_1) [AddMonoidWithOne R] (p : โ„•) [CharP R p] :
CharP (ULift.{u_2, u_1} R) p
source
๐Ÿ“ coverage
instance MulOpposite.charP (R : Type u_1) [AddMonoidWithOne R] (p : โ„•) [CharP R p] :
CharP Rแตแต’แต– p
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
instance Fin.charP (n : โ„•) [NeZero n] :
CharP (Fin n) n

The characteristic of F_p is p.

source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
instance instIsCharPOfIsLeftCancelAddOfCharP (ฮฑ : Type u_2) [Semiring ฮฑ] [IsLeftCancelAdd ฮฑ] (n : โ„•) [CharP ฮฑ n] :
Lean.Grind.IsCharP ฮฑ n