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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp]

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

↑n = 0 ↔ n = 0

@[simp, norm_cast]

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

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

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

@[simp]

theorem int.cast_eq_one {α : Type u_1} [add_group_with_one α] [char_zero α] {n : ℤ} :

↑n = 1 ↔ n = 1

theorem int.cast_ne_one {α : Type u_1} [add_group_with_one α] [char_zero α] {n : ℤ} :

@[simp, norm_cast]

theorem int.cast_div_char_zero {k : Type u_1} [division_ring k] [char_zero k] {m n : ℤ} (n_dvd : n ∣ m) :

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

Injectivity of int.cast into characteristic zero rings and fields. #