Torsion-free rings

A characteristic zero domain is torsion-free.

theorem IsDomain.instHasUniqueDivOfCharZero (R : Type u_1) [Semiring R] [IsDomain R] [CharZero R] : HasUniqueDiv R

theorem MonoidHom.map_neg_one {R : Type u_1} {M : Type u_2} [Ring R] [Monoid M] [IsMulTorsionFree M] (f : R →* M) : f (-1) = 1

@[simp]

theorem MonoidHom.map_neg {R : Type u_1} {M : Type u_2} [Ring R] [Monoid M] [IsMulTorsionFree M] (f : R →* M) (x : R) : f (-x) = f x

theorem MonoidHom.map_sub_swap {R : Type u_1} {M : Type u_2} [Ring R] [Monoid M] [IsMulTorsionFree M] (f : R →* M) (x y : R) : f (x - y) = f (y - x)