# 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 #

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

## TODO #

- Unify with `CharP` (possibly using an out-parameter)

source
class CharZero (R : Type u_1) [AddMonoidWithOne 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`, `CharZero R` and `CharP R 0` need not coincide.

- `CharZero R` requires an injection `ℕ ↪ R`;
- `CharP 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 `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does. This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.

- cast_injective : Function.Injective Nat.cast

  An additive monoid with one has characteristic zero if the canonical map `ℕ → R` is injective.

Instances

source
theorem charZero_of_inj_zero {R : Type u_1} [AddGroupWithOne R] (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
CharZero R
source
theorem Nat.cast_injective {R : Type u_1} [AddMonoidWithOne R] [CharZero R] :
Function.Injective Nat.cast
source
@[simp]
theorem Nat.cast_inj {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {m n : ℕ} :
↑m = ↑n ↔ m = n
source
@[simp]
theorem Nat.cast_eq_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
↑n = 0 ↔ n = 0
source
theorem Nat.cast_ne_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
↑n ≠ 0 ↔ n ≠ 0
source
theorem Nat.cast_add_one_ne_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) :
↑n + 1 ≠ 0
source
@[simp]
theorem Nat.cast_eq_one {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
↑n = 1 ↔ n = 1
source
theorem Nat.cast_ne_one {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
↑n ≠ 1 ↔ n ≠ 1
source
@[simp]
theorem OfNat.ofNat_ne_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
ofNat n ≠ 0
source
@[simp]
theorem OfNat.zero_ne_ofNat {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
0 ≠ ofNat n
source
@[simp]
theorem OfNat.ofNat_ne_one {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
ofNat n ≠ 1
source
@[simp]
theorem OfNat.one_ne_ofNat {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
1 ≠ ofNat n
source
@[simp]
theorem OfNat.ofNat_eq_ofNat {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] :
ofNat m = ofNat n ↔ ofNat m = ofNat n
source
instance NeZero.charZero {M : Type u_2} {n : ℕ} [NeZero n] [AddMonoidWithOne M] [CharZero M] :
NeZero ↑n
source
instance NeZero.charZero_one {M : Type u_2} [AddMonoidWithOne M] [CharZero M] :
NeZero 1
source
instance NeZero.charZero_ofNat {M : Type u_2} {n : ℕ} [n.AtLeastTwo] [AddMonoidWithOne M] [CharZero M] :
NeZero (OfNat.ofNat n)