Documentation

Mathlib.Data.Int.CharZero

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

@[simp]
theorem Int.cast_eq_zero {α : Type u_1} [inst : AddGroupWithOne α] [inst : CharZero α] {n : } :
n = 0 n = 0
@[simp]
theorem Int.cast_inj {α : Type u_1} [inst : AddGroupWithOne α] [inst : CharZero α] {m : } {n : } :
m = n m = n
theorem Int.cast_injective {α : Type u_1} [inst : AddGroupWithOne α] [inst : CharZero α] :
theorem Int.cast_ne_zero {α : Type u_1} [inst : AddGroupWithOne α] [inst : CharZero α] {n : } :
n 0 n 0
@[simp]
theorem Int.cast_div_charZero {k : Type u_1} [inst : DivisionRing k] [inst : CharZero k] {m : } {n : } (n_dvd : n m) :
↑(m / n) = m / n
theorem RingHom.injective_int {α : Type u_1} [inst : NonAssocRing α] (f : →+* α) [inst : CharZero α] :