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.

def Nat.castEmbedding {R : Type u_1} [AddMonoidWithOne R] [CharZero R] : ℕ ↪ R

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

Equations

• Nat.castEmbedding = { toFun := Nat.cast, inj' := ⋯ }

@[simp]

theorem Nat.castEmbedding_apply {R : Type u_1} [AddMonoidWithOne R] [CharZero R] : ∀ (a : ℕ), Nat.castEmbedding a = ↑a

@[simp]

theorem Nat.cast_pow_eq_one {R : Type u_2} [Semiring R] [CharZero R] (q : ℕ) (n : ℕ) (hn : n ≠ 0) : ↑q ^ n = 1 ↔ q = 1

@[simp]

theorem Nat.cast_div_charZero {k : Type u_2} [DivisionSemiring k] [CharZero k] {m : ℕ} {n : ℕ} (n_dvd : n ∣ m) : ↑(m / n) = ↑m / ↑n

instance CharZero.NeZero.two {M : Type u_2} [AddMonoidWithOne M] [CharZero M] : NeZero 2

Equations

• ⋯ = ⋯

theorem Function.support_natCast {α : Type u_1} {M : Type u_2} [AddMonoidWithOne M] [CharZero M] {n : ℕ} (hn : n ≠ 0) : Function.support ↑n = Set.univ

@[deprecated Function.support_natCast]

theorem Function.support_nat_cast {α : Type u_1} {M : Type u_2} [AddMonoidWithOne M] [CharZero M] {n : ℕ} (hn : n ≠ 0) : Function.support ↑n = Set.univ

Alias of Function.support_natCast.

theorem Function.mulSupport_natCast {α : Type u_1} {M : Type u_2} [AddMonoidWithOne M] [CharZero M] {n : ℕ} (hn : n ≠ 1) : Function.mulSupport ↑n = Set.univ

@[deprecated Function.mulSupport_natCast]

theorem Function.mulSupport_nat_cast {α : Type u_1} {M : Type u_2} [AddMonoidWithOne M] [CharZero M] {n : ℕ} (hn : n ≠ 1) : Function.mulSupport ↑n = Set.univ

Alias of Function.mulSupport_natCast.

@[simp]

theorem add_self_eq_zero {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} : a + a = 0 ↔ a = 0

theorem CharZero.neg_eq_self_iff {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} : -a = a ↔ a = 0

theorem CharZero.eq_neg_self_iff {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} : a = -a ↔ a = 0

theorem nat_mul_inj {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a : R} {b : R} (h : ↑n * a = ↑n * b) : n = 0 ∨ a = b

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

@[simp]

theorem add_self_div_two {R : Type u_1} [DivisionSemiring R] [NeZero 2] (a : R) : (a + a) / 2 = a

@[deprecated add_self_div_two]

theorem half_add_self {R : Type u_1} [DivisionSemiring R] [NeZero 2] (a : R) : (a + a) / 2 = a

Alias of add_self_div_two.

@[simp]

theorem add_halves {R : Type u_1} [DivisionSemiring R] [NeZero 2] (a : R) : a / 2 + a / 2 = a

@[deprecated add_halves]

theorem add_halves' {R : Type u_1} [DivisionSemiring R] [NeZero 2] (a : R) : a / 2 + a / 2 = a

Alias of add_halves.

theorem sub_half {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) : a - a / 2 = a / 2

theorem half_sub {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) : a / 2 - a = -(a / 2)

instance WithTop.instCharZero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] : CharZero (WithTop R)

Equations

• ⋯ = ⋯

instance WithBot.instCharZero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] : CharZero (WithBot R)

Equations

• ⋯ = ⋯

theorem RingHom.charZero {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] (ϕ : R →+* S) [CharZero S] : CharZero R

theorem RingHom.charZero_iff {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] {ϕ : R →+* S} (hϕ : Function.Injective ⇑ϕ) : CharZero R ↔ CharZero S

theorem RingHom.injective_nat {R : Type u_1} [NonAssocSemiring R] (f : ℕ →+* R) [CharZero R] : Function.Injective ⇑f

@[simp]

theorem units_ne_neg_self {R : Type u_1} [Ring R] [CharZero R] (u : Rˣ) : u ≠ -u

@[simp]

theorem neg_units_ne_self {R : Type u_1} [Ring R] [CharZero R] (u : Rˣ) : -u ≠ u