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 #

A linearly ordered semiring has characteristic zero.
Characteristic zero implies that the additive monoid is infinite.

TODO #

Once order of a group is defined for infinite additive monoids redefine or at least connect to order of 1 in the additive monoid with one.
Unify with char_p (possibly using an out-parameter)

@[class]

structure char_zero (R : Type u_1) [add_monoid R] [has_one R] :

Prop

cast_injective : function.injective coe

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

Instances

theorem char_zero_of_inj_zero {R : Type u_1} [add_left_cancel_monoid R] [has_one R] (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :

theorem ordered_semiring.to_char_zero {R : Type u_1} [ordered_semiring R] [nontrivial R] :

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

@[protected, instance]

def linear_ordered_semiring.to_char_zero {R : Type u_1} [linear_ordered_semiring R] :

theorem nat.cast_injective {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] :

function.injective coe

@[simp]

theorem nat.cast_embedding_apply {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] (ᾰ : ℕ) :

⇑nat.cast_embedding ᾰ = ↑ᾰ

def nat.cast_embedding {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] :

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

Equations

nat.cast_embedding = {to_fun := coe coe_to_lift, inj' := _}

@[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

@[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

@[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

theorem nat.cast_add_one_ne_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] (n : ℕ) :

↑n + 1 ≠ 0

@[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

@[protected, instance]

def char_zero.infinite (M : Type u_1) [add_monoid M] [has_one M] [char_zero M] :

theorem two_ne_zero' {M : Type u_1} [add_monoid M] [has_one M] [char_zero M] :

2 ≠ 0

@[simp]

theorem add_self_eq_zero {R : Type u_1} [semiring R] [no_zero_divisors R] [char_zero R] {a : R} :

a + a = 0 ↔ a = 0

@[simp]

theorem bit0_eq_zero {R : Type u_1} [semiring R] [no_zero_divisors R] [char_zero R] {a : R} :

bit0 a = 0 ↔ a = 0

@[simp]

theorem zero_eq_bit0 {R : Type u_1} [semiring R] [no_zero_divisors R] [char_zero R] {a : R} :

0 = bit0 a ↔ a = 0

theorem neg_eq_self_iff {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {a : R} :

-a = a ↔ a = 0

theorem eq_neg_self_iff {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {a : R} :

a = -a ↔ a = 0

theorem nat_mul_inj {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {n : ℕ} {a b : R} (h : (↑n) * a = (↑n) * b) :

n = 0 ∨ a = b

theorem nat_mul_inj' {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {n : ℕ} {a b : R} (h : (↑n) * a = (↑n) * b) (w : n ≠ 0) :

a = b

theorem bit0_injective {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] :

function.injective bit0

theorem bit1_injective {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] :

function.injective bit1

@[simp]

theorem bit0_eq_bit0 {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {a b : R} :

bit0 a = bit0 b ↔ a = b

@[simp]

theorem bit1_eq_bit1 {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {a b : R} :

bit1 a = bit1 b ↔ a = b

@[simp]

theorem bit1_eq_one {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {a : R} :

bit1 a = 1 ↔ a = 0

@[simp]

theorem one_eq_bit1 {R : Type u_1} [ring R] [no_zero_divisors R] [char_zero R] {a : R} :

1 = bit1 a ↔ a = 0

@[simp]

theorem half_add_self {R : Type u_1} [division_ring R] [char_zero R] (a : R) :

(a + a) / 2 = a

@[simp]

theorem add_halves' {R : Type u_1} [division_ring R] [char_zero R] (a : R) :

a / 2 + a / 2 = a

theorem sub_half {R : Type u_1} [division_ring R] [char_zero R] (a : R) :

a - a / 2 = a / 2

theorem half_sub {R : Type u_1} [division_ring R] [char_zero R] (a : R) :

a / 2 - a = -(a / 2)

@[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)

theorem ring_hom.char_zero {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (ϕ : R →+* S) [hS : char_zero S] :

theorem ring_hom.char_zero_iff {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {ϕ : R →+* S} (hϕ : function.injective ⇑ϕ) :

char_zero R ↔ char_zero S