mathlib3 documentation

algebra.char_zero.lemmas

Characteristic zero (additional theorems) #

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

Characteristic zero implies that the additive monoid is infinite.

@[simp]

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

⇑nat.cast_embedding ᾰ = ↑ᾰ

def nat.cast_embedding {R : Type u_1} [add_monoid_with_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]

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

@[simp, norm_cast]

theorem nat.cast_div_char_zero {k : Type u_1} [division_semiring k] [char_zero k] {m n : ℕ} (n_dvd : n ∣ m) :

↑(m / n) = ↑m / ↑n

@[protected, instance]

def char_zero.ne_zero.two (M : Type u_1) [add_monoid_with_one M] [char_zero M] :

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

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

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

theorem bit0_ne_zero {R : Type u_1} [non_assoc_semiring R] [no_zero_divisors R] [char_zero R] {a : R} :

bit0 a ≠ 0 ↔ a ≠ 0

theorem zero_ne_bit0 {R : Type u_1} [non_assoc_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} [non_assoc_ring R] [no_zero_divisors R] [char_zero R] {a : R} :

-a = a ↔ a = 0

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

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

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

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

function.injective bit0

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

function.injective bit1

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

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

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

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

@[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_with_one R] [char_zero R] :

char_zero (with_top R)

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] :

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

theorem ring_hom.injective_nat {R : Type u_1} [non_assoc_semiring R] (f : ℕ →+* R) [char_zero R] :

function.injective ⇑f