mathlib3 documentation

algebra.char_zero.defs

Characteristic zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

TODO #

source
@[class]
structure char_zero (R : Type u_1) [add_monoid_with_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 of this typeclass
source
theorem char_zero_of_inj_zero {R : Type u_1} [add_group_with_one R] (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
char_zero R
source
theorem nat.cast_injective {R : Type u_1} [add_monoid_with_one R] [char_zero R] :
function.injective coe
source
@[simp, norm_cast]
theorem nat.cast_inj {R : Type u_1} [add_monoid_with_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_with_one R] [char_zero R] {n : ℕ} :
↑n = 0 ↔ n = 0
source
@[norm_cast]
theorem nat.cast_ne_zero {R : Type u_1} [add_monoid_with_one R] [char_zero R] {n : ℕ} :
↑n ≠ 0 ↔ n ≠ 0
source
theorem nat.cast_add_one_ne_zero {R : Type u_1} [add_monoid_with_one R] [char_zero R] (n : ℕ) :
↑n + 1 ≠ 0
source
@[simp, norm_cast]
theorem nat.cast_eq_one {R : Type u_1} [add_monoid_with_one R] [char_zero R] {n : ℕ} :
↑n = 1 ↔ n = 1
source
@[norm_cast]
theorem nat.cast_ne_one {R : Type u_1} [add_monoid_with_one R] [char_zero R] {n : ℕ} :
↑n ≠ 1 ↔ n ≠ 1
source
@[protected, instance]
def ne_zero.char_zero {M : Type u_1} {n : ℕ} [ne_zero n] [add_monoid_with_one M] [char_zero M] :
ne_zero ↑n