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 #

source
@[simp]
theorem Nat.castEmbedding_apply {R : Type u_1} [AddMonoidWithOne R] [CharZero R] :
∀ (a : ℕ), Nat.castEmbedding a = ↑a
source
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' := ⋯ }
source
@[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
source
@[simp]
theorem Nat.cast_div_charZero {k : Type u_2} [DivisionSemiring k] [CharZero k] {m : ℕ} {n : ℕ} (n_dvd : n ∣ m) :
↑(m / n) = ↑m / ↑n
source
instance CharZero.NeZero.two {M : Type u_2} [AddMonoidWithOne M] [CharZero M] :
NeZero 2
Equations
  • ⋯ = ⋯
source
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
source
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
source
@[simp]
theorem add_self_eq_zero {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
a + a = 0 ↔ a = 0
source
@[simp]
theorem bit0_eq_zero {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
bit0 a = 0 ↔ a = 0
source
@[simp]
theorem zero_eq_bit0 {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
0 = bit0 a ↔ a = 0
source
theorem bit0_ne_zero {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
bit0 a ≠ 0 ↔ a ≠ 0
source
theorem zero_ne_bit0 {R : Type u_1} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
0 ≠ bit0 a ↔ a ≠ 0
source
@[simp]
theorem neg_eq_self_iff {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
-a = a ↔ a = 0
source
@[simp]
theorem eq_neg_self_iff {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
a = -a ↔ a = 0
source
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
source
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
source
theorem bit0_injective {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] :
Function.Injective bit0
source
theorem bit1_injective {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] :
Function.Injective bit1
source
@[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
source
@[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
source
@[simp]
theorem bit1_eq_one {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
bit1 a = 1 ↔ a = 0
source
@[simp]
theorem one_eq_bit1 {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
1 = bit1 a ↔ a = 0
source
@[simp]
theorem half_add_self {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) :
(a + a) / 2 = a
source
@[simp]
theorem add_halves' {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) :
a / 2 + a / 2 = a
source
theorem sub_half {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) :
a - a / 2 = a / 2
source
theorem half_sub {R : Type u_1} [DivisionRing R] [CharZero R] (a : R) :
a / 2 - a = -(a / 2)
source
instance WithTop.instCharZeroWithTopAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] [CharZero R] :
CharZero (WithTop R)
Equations
  • ⋯ = ⋯
source
instance WithBot.instCharZeroWithBotAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] [CharZero R] :
CharZero (WithBot R)
Equations
  • ⋯ = ⋯
source
theorem RingHom.charZero {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] (ϕ : R →+* S) [hS : CharZero S] :
CharZero R
source
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
source
theorem RingHom.injective_nat {R : Type u_1} [NonAssocSemiring R] (f : ℕ →+* R) [CharZero R] :
Function.Injective ⇑f
source
@[simp]
theorem units_ne_neg_self {R : Type u_1} [Ring R] [CharZero R] (u : Rˣ) :
u ≠ -u
source
@[simp]
theorem neg_units_ne_self {R : Type u_1} [Ring R] [CharZero R] (u : Rˣ) :
-u ≠ u