Documentation

Mathlib.Data.Int.CharZero

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 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.