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)
:
@[simp]
theorem
Int.cast_div_ofNat_charZero
{k : Type u_3}
[DivisionRing k]
[CharZero k]
{m n : ℕ}
(n_dvd : n ∣ m)
:
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.