Documentation

Mathlib.Data.Int.CharZero

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_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_3} [DivisionRing k] [CharZero k] {m : } {n : } (n_dvd : n m) :
(m / n) = m / n
@[simp]
theorem Int.cast_div_ofNat_charZero {k : Type u_3} [DivisionRing k] [CharZero k] {m : } {n : } (n_dvd : n m) :
(m / n) = m / n
theorem Function.support_int_cast {α : Type u_1} {β : Type u_2} [AddGroupWithOne β] [CharZero β] {n : } (hn : n 0) :
Function.support n = Set.univ
theorem Function.mulSupport_int_cast {α : Type u_1} {β : Type u_2} [AddGroupWithOne β] [CharZero β] {n : } (hn : n 1) :
Function.mulSupport n = Set.univ