mathlib3 documentation

data.int.char_zero

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 : } :
m = n m = n
theorem int.cast_ne_zero {α : Type u_1} [add_group_with_one α] [char_zero α] {n : } :
n 0 n 0
@[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 : } :
n 1 n 1
@[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) :
(m / n) = m / n