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)
:
theorem
Function.mulSupport_intCast
{α : Type u_1}
{β : Type u_2}
[AddGroupWithOne β]
[CharZero β]
{n : ℤ}
(hn : n ≠ 1)
:
mulSupport ↑n = Set.univ