Injectivity of Int.Cast into characteristic zero rings and fields.

@[simp]

theorem Int.cast_eq_zero {α : Type u_1} [AddGroupWithOne α] [CharZero α] {n : ℤ} : ↑n = 0 ↔ n = 0

@[simp]

theorem Int.cast_inj {α : Type u_1} [AddGroupWithOne α] [CharZero α] {m : ℤ} {n : ℤ} : ↑m = ↑n ↔ m = n

theorem Int.cast_injective {α : Type u_1} [AddGroupWithOne α] [CharZero α] : Function.Injective Int.cast

theorem Int.cast_ne_zero {α : Type u_1} [AddGroupWithOne α] [CharZero α] {n : ℤ} : ↑n ≠ 0 ↔ n ≠ 0

@[simp]

theorem Int.cast_eq_one {α : Type u_1} [AddGroupWithOne α] [CharZero α] {n : ℤ} : ↑n = 1 ↔ n = 1

theorem Int.cast_ne_one {α : Type u_1} [AddGroupWithOne α] [CharZero α] {n : ℤ} : ↑n ≠ 1 ↔ n ≠ 1

@[simp]

theorem Int.cast_div_charZero {k : Type u_2} [DivisionRing k] [CharZero k] {m : ℤ} {n : ℤ} (n_dvd : n ∣ m) : ↑(m / n) = ↑m / ↑n

@[simp]

theorem Int.cast_div_ofNat_charZero {k : Type u_2} [DivisionRing k] [CharZero k] {m : ℕ} {n : ℕ} (n_dvd : n ∣ m) : ↑(↑m / ↑n) = ↑m / ↑n

theorem RingHom.injective_int {α : Type u_2} [NonAssocRing α] (f : ℤ →+* α) [CharZero α] : Function.Injective ⇑f