mathlib documentation

algebra.char_zero

Characteristic zero #

A ring R is called of characteristic zero if every natural number n is non-zero when considered as an element of R. Since this definition doesn't mention the multiplicative structure of R except for the existence of 1 in this file characteristic zero is defined for additive monoids with 1.

Main definition #

char_zero is the typeclass of an additive monoid with one such that the natural homomorphism from the natural numbers into it is injective.

Main statements #

TODO #

source
@[class]
structure char_zero (R : Type u_1) [add_monoid R] [has_one R] :
Prop

Typeclass for monoids with characteristic zero. (This is usually stated on fields but it makes sense for any additive monoid with 1.)

Warning: for a semiring R, char_zero R and char_p R 0 need not coincide.

  • char_zero R requires an injection ℕ ↪ R;
  • char_p R 0 asks that only 0 : ℕ maps to 0 : R under the map ℕ → R.

For instance, endowing {0, 1} with addition given by max (i.e. 1 is absorbing), shows that char_zero {0, 1} does not hold and yet char_p {0, 1} 0 does. This example is formalized in counterexamples/char_p_zero_ne_char_zero.

Instances
source
theorem char_zero_of_inj_zero {R : Type u_1} [add_left_cancel_monoid R] [has_one R] (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
char_zero R
source
theorem ordered_semiring.to_char_zero {R : Type u_1} [ordered_semiring R] [nontrivial R] :
char_zero R

Note this is not an instance as char_zero implies nontrivial, and this would risk forming a loop.

source
@[protected, instance]
def linear_ordered_semiring.to_char_zero {R : Type u_1} [linear_ordered_semiring R] :
char_zero R
source
theorem nat.cast_injective {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] :
function.injective coe
source
@[simp]
theorem nat.cast_embedding_apply {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] (ᾰ : ℕ) :
⇑nat.cast_embedding ᾰ = ↑ᾰ
source
def nat.cast_embedding {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] :
ℕ ↪ R

nat.cast as an embedding into monoids of characteristic 0.

Equations
source
@[simp, norm_cast]
theorem nat.cast_inj {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {m n : ℕ} :
↑m = ↑n ↔ m = n
source
@[simp, norm_cast]
theorem nat.cast_eq_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {n : ℕ} :
↑n = 0 ↔ n = 0
source
@[simp, norm_cast]
theorem nat.cast_eq_one {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {n : ℕ} :
↑n = 1 ↔ n = 1
source
@[simp]
theorem nat.cast_pow_eq_one {R : Type u_1} [semiring R] [char_zero R] (q n : ℕ) (hn : n ≠ 0) :
↑q ^ n = 1 ↔ q = 1
source
@[norm_cast]
theorem nat.cast_ne_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {n : ℕ} :
↑n ≠ 0 ↔ n ≠ 0
source
@[norm_cast]
theorem nat.cast_ne_one {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {n : ℕ} :
↑n ≠ 1 ↔ n ≠ 1
source
theorem nat.cast_add_one_ne_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] (n : ℕ) :
↑n + 1 ≠ 0
source
@[simp, norm_cast]
theorem nat.cast_dvd_char_zero {k : Type u_1} [field k] [char_zero k] {m n : ℕ} (n_dvd : n ∣ m) :
↑(m / n) = ↑m / ↑n
source
@[protected, instance]
def char_zero.infinite (M : Type u_1) [add_monoid M] [has_one M] [char_zero M] :
infinite M
source
theorem two_ne_zero' {M : Type u_1} [add_monoid M] [has_one M] [char_zero M] :
2 ≠ 0
source
@[simp]
theorem add_self_eq_zero {R : Type u_1} [non_assoc_semiring R] [no_zero_divisors R] [char_zero R] {a : R} :
a + a = 0 ↔ a = 0
source
@[simp]
theorem bit0_eq_zero {R : Type u_1} [non_assoc_semiring R] [no_zero_divisors R] [char_zero R] {a : R} :
bit0 a = 0 ↔ a = 0
source
@[simp]
theorem zero_eq_bit0 {R : Type u_1} [non_assoc_semiring R] [no_zero_divisors R] [char_zero R] {a : R} :
0 = bit0 a ↔ a = 0
source
theorem neg_eq_self_iff {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {a : R} :
-a = a ↔ a = 0
source
theorem eq_neg_self_iff {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {a : R} :
a = -a ↔ a = 0
source
theorem nat_mul_inj {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {n : ℕ} {a b : R} (h : (↑n) * a = (↑n) * b) :
n = 0 ∨ a = b
source
theorem nat_mul_inj' {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {n : ℕ} {a b : R} (h : (↑n) * a = (↑n) * b) (w : n ≠ 0) :
a = b
source
theorem bit0_injective {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] :
function.injective bit0
source
theorem bit1_injective {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] :
function.injective bit1
source
@[simp]
theorem bit0_eq_bit0 {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {a b : R} :
bit0 a = bit0 b ↔ a = b
source
@[simp]
theorem bit1_eq_bit1 {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {a b : R} :
bit1 a = bit1 b ↔ a = b
source
@[simp]
theorem bit1_eq_one {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {a : R} :
bit1 a = 1 ↔ a = 0
source
@[simp]
theorem one_eq_bit1 {R : Type u_1} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {a : R} :
1 = bit1 a ↔ a = 0
source
@[simp]
theorem half_add_self {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
(a + a) / 2 = a
source
@[simp]
theorem add_halves' {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
a / 2 + a / 2 = a
source
theorem sub_half {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
a - a / 2 = a / 2
source
theorem half_sub {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
a / 2 - a = -(a / 2)
source
@[protected, instance]
def with_top.char_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] :
char_zero (with_top R)
source
theorem ring_hom.char_zero {R : Type u_1} {S : Type u_2} [non_assoc_semiring R] [non_assoc_semiring S] (ϕ : R →+* S) [hS : char_zero S] :
char_zero R
source
theorem ring_hom.char_zero_iff {R : Type u_1} {S : Type u_2} [non_assoc_semiring R] [non_assoc_semiring S] {ϕ : R →+* S} (hϕ : function.injective ⇑ϕ) :
char_zero R ↔ char_zero S