Documentation

Mathlib.Algebra.Ring.CharZero

Characteristic zero rings #

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

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

Equations
    Instances For
      source
      @[simp]
      theorem Nat.castEmbedding_apply {R : Type u_2} [AddMonoidWithOne R] [CharZero R] (a✝ : ℕ) :
      castEmbedding a✝ = ↑a✝
      source
      instance CharZero.NeZero.two {R : Type u_2} [AddMonoidWithOne R] [CharZero R] :
      NeZero 2
      source
      theorem Function.support_natCast {α : Type u_1} {R : Type u_2} {n : ℕ} [AddMonoidWithOne R] [CharZero R] (hn : n ≠ 0) :
      support ↑n = Set.univ
      source
      theorem Function.mulSupport_natCast {α : Type u_1} {R : Type u_2} {n : ℕ} [AddMonoidWithOne R] [CharZero R] (hn : n ≠ 1) :
      mulSupport ↑n = Set.univ
      source
      theorem RingHom.charZero {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] (ϕ : R →+* S) [CharZero S] :
      CharZero R
      source
      theorem RingHom.charZero_iff {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] {ϕ : R →+* S} (hϕ : Function.Injective ⇑ϕ) :
      CharZero R ↔ CharZero S
      source
      theorem RingHom.injective_nat {R : Type u_2} [NonAssocSemiring R] (f : ℕ →+* R) [CharZero R] :
      Function.Injective ⇑f
      source
      @[simp]
      theorem add_self_eq_zero {R : Type u_2} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} :
      a + a = 0 ↔ a = 0
      source
      @[simp]
      theorem Nat.cast_pow_eq_one {R : Type u_2} {n : ℕ} [Semiring R] [CharZero R] {a : ℕ} (hn : n ≠ 0) :
      ↑a ^ n = 1 ↔ a = 1
      source
      theorem CharZero.neg_eq_self_iff {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
      -a = a ↔ a = 0
      source
      theorem CharZero.eq_neg_self_iff {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} :
      a = -a ↔ a = 0
      source
      theorem nat_mul_inj {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R} (h : ↑n * a = ↑n * b) :
      n = 0 ∨ a = b
      source
      theorem nat_mul_inj' {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R} (h : ↑n * a = ↑n * b) (w : n ≠ 0) :
      a = b
      source
      @[simp]
      theorem units_ne_neg_self {R : Type u_2} [Ring R] [CharZero R] (u : Rˣ) :
      u ≠ -u
      source
      @[simp]
      theorem neg_units_ne_self {R : Type u_2} [Ring R] [CharZero R] (u : Rˣ) :
      -u ≠ u