Characteristic zero rings #
Nat.cast as an embedding into monoids of characteristic 0.
Instances For
@[simp]
theorem
Nat.castEmbedding_apply
{R : Type u_2}
[AddMonoidWithOne R]
[CharZero R]
(a✝ : ℕ)
:
castEmbedding a✝ = ↑a✝
theorem
Function.support_natCast
{α : Type u_1}
{R : Type u_2}
{n : ℕ}
[AddMonoidWithOne R]
[CharZero R]
(hn : n ≠ 0)
:
theorem
Function.mulSupport_natCast
{α : Type u_1}
{R : Type u_2}
{n : ℕ}
[AddMonoidWithOne R]
[CharZero R]
(hn : n ≠ 1)
:
mulSupport ↑n = Set.univ
theorem
RingHom.charZero
{R : Type u_2}
{S : Type u_3}
[NonAssocSemiring R]
[NonAssocSemiring S]
(ϕ : R →+* S)
[CharZero S]
:
CharZero R
theorem
RingHom.charZero_iff
{R : Type u_2}
{S : Type u_3}
[NonAssocSemiring R]
[NonAssocSemiring S]
{ϕ : R →+* S}
(hϕ : Function.Injective ⇑ϕ)
:
theorem
RingHom.injective_nat
{R : Type u_2}
[NonAssocSemiring R]
(f : ℕ →+* R)
[CharZero R]
:
Function.Injective ⇑f
@[simp]
theorem
add_self_eq_zero
{R : Type u_2}
[NonAssocSemiring R]
[NoZeroDivisors R]
[CharZero R]
{a : R}
:
a + a = 0 ↔ a = 0
@[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
@[instance 100]
instance
IsAddTorsionFree.of_isCancelMulZero_charZero
{R : Type u_2}
[Semiring R]
[CharZero R]
[IsCancelMulZero R]
:
A characteristic zero domain is torsion-free.
theorem
CharZero.neg_eq_self_iff
{R : Type u_2}
[NonAssocRing R]
[NoZeroDivisors R]
[CharZero R]
{a : R}
:
-a = a ↔ a = 0
theorem
CharZero.eq_neg_self_iff
{R : Type u_2}
[NonAssocRing R]
[NoZeroDivisors R]
[CharZero R]
{a : R}
:
a = -a ↔ a = 0
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
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