Documentation

Mathlib.Algebra.CharZero.Lemmas

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 #

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

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

Equations
  • Nat.castEmbedding = { toFun := Nat.cast, inj' := }
Instances For
    @[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
    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
    @[simp]
    theorem bit0_eq_zero {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
    bit0 a = 0 a = 0
    @[simp]
    theorem zero_eq_bit0 {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
    0 = bit0 a a = 0
    theorem bit0_ne_zero {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
    bit0 a 0 a 0
    theorem zero_ne_bit0 {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
    0 bit0 a a 0
    @[simp]
    theorem neg_eq_self_iff {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
    -a = a a = 0
    @[simp]
    theorem 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 bit0_eq_bit0 {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} {b : R} :
    bit0 a = bit0 b a = b
    @[simp]
    theorem bit1_eq_bit1 {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} {b : R} :
    bit1 a = bit1 b a = b
    @[simp]
    theorem bit1_eq_one {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
    bit1 a = 1 a = 0
    @[simp]
    theorem one_eq_bit1 {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
    1 = bit1 a a = 0
    @[simp]
    theorem half_add_self {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) :
    (a + a) / 2 = a
    @[simp]
    theorem add_halves' {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) :
    a / 2 + a / 2 = a
    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)
    Equations
    • =
    Equations
    • =
    theorem RingHom.charZero {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] (ϕ : R →+* S) [CharZero S] :
    theorem RingHom.charZero_iff {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] {ϕ : R →+* S} (hϕ : Function.Injective ϕ) :
    @[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