# Documentation

Mathlib.Algebra.CharZero.Defs

# 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)
class CharZero (R : Type u_1) [inst : ] :
• An additive monoid with one has characteristic zero if the canonical map ℕ → R→ R is injective.

cast_injective : Function.Injective Nat.cast

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↪ R;
• CharP R 0 asks that only 0 : ℕ maps to 0 : R under the map ℕ → R→ 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/char_p_zero_ne_char_zero.
Instances
theorem charZero_of_inj_zero {R : Type u_1} [inst : ] (H : ∀ (n : ), n = 0n = 0) :
theorem Nat.cast_injective {R : Type u_1} [inst : ] [inst : ] :
@[simp]
theorem Nat.cast_inj {R : Type u_1} [inst : ] [inst : ] {m : } {n : } :
m = n m = n
@[simp]
theorem Nat.cast_eq_zero {R : Type u_1} [inst : ] [inst : ] {n : } :
n = 0 n = 0
theorem Nat.cast_ne_zero {R : Type u_1} [inst : ] [inst : ] {n : } :
n 0 n 0
theorem Nat.cast_add_one_ne_zero {R : Type u_1} [inst : ] [inst : ] (n : ) :
n + 1 0
@[simp]
theorem Nat.cast_eq_one {R : Type u_1} [inst : ] [inst : ] {n : } :
n = 1 n = 1
theorem Nat.cast_ne_one {R : Type u_1} [inst : ] [inst : ] {n : } :
n 1 n 1
@[simp]
theorem OfNat.ofNat_ne_zero {R : Type u_1} [inst : ] [inst : ] (n : ) [h : ] :
0
@[simp]
theorem OfNat.zero_ne_ofNat {R : Type u_1} [inst : ] [inst : ] (n : ) [inst : ] :
0
@[simp]
theorem OfNat.ofNat_ne_one {R : Type u_1} [inst : ] [inst : ] (n : ) [h : ] :
1
@[simp]
theorem OfNat.one_ne_ofNat {R : Type u_1} [inst : ] [inst : ] (n : ) [inst : ] :
1
@[simp]
theorem OfNat.ofNat_eq_ofNat {R : Type u_1} [inst : ] [inst : ] {m : } {n : } [inst : ] [inst : ] :
instance NeZero.charZero {M : Type u_1} {n : } [inst : ] [inst : ] [inst : ] :
NeZero n
Equations
instance NeZero.charZero_ofNat {M : Type u_1} {n : } [inst : ] [inst : ] [inst : ] :
Equations