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.castEmbedding = { toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) }
instance
CharZero.NeZero.two
(M : Type u_1)
[inst : AddMonoidWithOne M]
[inst : CharZero M]
:
NeZero 2
@[simp]
theorem
add_self_eq_zero
{R : Type u_1}
[inst : NonAssocSemiring R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
@[simp]
theorem
bit0_eq_zero
{R : Type u_1}
[inst : NonAssocSemiring R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
@[simp]
theorem
zero_eq_bit0
{R : Type u_1}
[inst : NonAssocSemiring R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
theorem
bit0_ne_zero
{R : Type u_1}
[inst : NonAssocSemiring R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
theorem
zero_ne_bit0
{R : Type u_1}
[inst : NonAssocSemiring R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
theorem
neg_eq_self_iff
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
theorem
eq_neg_self_iff
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
theorem
nat_mul_inj
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{n : ℕ}
{a : R}
{b : R}
(h : ↑n * a = ↑n * b)
:
theorem
nat_mul_inj'
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{n : ℕ}
{a : R}
{b : R}
(h : ↑n * a = ↑n * b)
(w : n ≠ 0)
:
a = b
theorem
bit0_injective
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
:
Function.Injective bit0
theorem
bit1_injective
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
:
Function.Injective bit1
@[simp]
theorem
bit0_eq_bit0
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
{b : R}
:
@[simp]
theorem
bit1_eq_bit1
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
{b : R}
:
@[simp]
theorem
bit1_eq_one
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
@[simp]
theorem
one_eq_bit1
{R : Type u_1}
[inst : NonAssocRing R]
[inst : NoZeroDivisors R]
[inst : CharZero R]
{a : R}
:
@[simp]
@[simp]
instance
WithTop.instCharZeroWithTopAddMonoidWithOne
{R : Type u_1}
[inst : AddMonoidWithOne R]
[inst : CharZero R]
:
theorem
RingHom.charZero
{R : Type u_1}
{S : Type u_2}
[inst : NonAssocSemiring R]
[inst : NonAssocSemiring S]
(ϕ : R →+* S)
[hS : CharZero S]
:
CharZero R
theorem
RingHom.charZero_iff
{R : Type u_1}
{S : Type u_2}
[inst : NonAssocSemiring R]
[inst : NonAssocSemiring S]
{ϕ : R →+* S}
(hϕ : Function.Injective ↑ϕ)
:
theorem
RingHom.injective_nat
{R : Type u_1}
[inst : NonAssocSemiring R]
(f : ℕ →+* R)
[inst : CharZero R]
: