Characteristic zero (additional theorems) #
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]
nat.cast as an embedding into monoids of characteristic 0.
Equations
- nat.cast_embedding = {to_fun := coe coe_to_lift, inj' := _}
@[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} :
@[simp]
theorem
bit0_eq_zero
{R : Type u_1}
[non_assoc_semiring R]
[no_zero_divisors R]
[char_zero R]
{a : R} :
@[simp]
theorem
zero_eq_bit0
{R : Type u_1}
[non_assoc_semiring R]
[no_zero_divisors R]
[char_zero R]
{a : R} :
theorem
neg_eq_self_iff
{R : Type u_1}
[non_assoc_ring R]
[no_zero_divisors R]
[char_zero R]
{a : R} :
theorem
eq_neg_self_iff
{R : Type u_1}
[non_assoc_ring R]
[no_zero_divisors R]
[char_zero R]
{a : R} :
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) :
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} :
@[simp]
theorem
bit1_eq_bit1
{R : Type u_1}
[non_assoc_ring R]
[no_zero_divisors R]
[char_zero R]
{a b : R} :
@[simp]
@[simp]
@[simp]
@[simp]
@[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] :
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 ⇑ϕ) :