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 #

@[simp]

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

Equations
@[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]
@[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
@[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]
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] :