Injectivity of Int.Cast
into characteristic zero rings and fields. #
@[simp]
theorem
Int.cast_injective
{α : Type u_1}
[inst : AddGroupWithOne α]
[inst : CharZero α]
:
Function.Injective Int.cast
theorem
RingHom.injective_int
{α : Type u_1}
[inst : NonAssocRing α]
(f : ℤ →+* α)
[inst : CharZero α]
: