mathlib documentation

data.int.char_zero

Injectivity of `int.cast` into characteristic zero rings. #

@[simp]

theorem int.cast_eq_zero {α : Type u_1} [add_group α] [has_one α] [char_zero α] {n : ℤ} :

↑n = 0 ↔ n = 0

@[simp, norm_cast]

theorem int.cast_inj {α : Type u_1} [add_group α] [has_one α] [char_zero α] {m n : ℤ} :

↑m = ↑n ↔ m = n

theorem int.cast_injective {α : Type u_1} [add_group α] [has_one α] [char_zero α] :

function.injective coe

theorem int.cast_ne_zero {α : Type u_1} [add_group α] [has_one α] [char_zero α] {n : ℤ} :

↑n ≠ 0 ↔ n ≠ 0

theorem ring_hom.injective_int {α : Type u_1} [ring α] (f : ℤ →+* α) [char_zero α] :

function.injective ⇑f