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

@[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 RingHom.injective_int {α : Type u_3} [NonAssocRing α] (f : ℤ →+* α) [CharZero α] : Function.Injective ⇑f

theorem Function.support_intCast {α : Type u_1} {β : Type u_2} [AddGroupWithOne β] [CharZero β] {n : ℤ} (hn : n ≠ 0) : Function.support ↑n = Set.univ

@[deprecated Function.support_intCast]

theorem Function.support_int_cast {α : Type u_1} {β : Type u_2} [AddGroupWithOne β] [CharZero β] {n : ℤ} (hn : n ≠ 0) : Function.support ↑n = Set.univ

Alias of Function.support_intCast.

theorem Function.mulSupport_intCast {α : Type u_1} {β : Type u_2} [AddGroupWithOne β] [CharZero β] {n : ℤ} (hn : n ≠ 1) : Function.mulSupport ↑n = Set.univ

@[deprecated Function.mulSupport_intCast]

theorem Function.mulSupport_int_cast {α : Type u_1} {β : Type u_2} [AddGroupWithOne β] [CharZero β] {n : ℤ} (hn : n ≠ 1) : Function.mulSupport ↑n = Set.univ

Alias of Function.mulSupport_intCast.