Torsion-free monoids with zero

We prove that if M is an UniqueFactorizationMonoid that can be equipped with a NormalizationMonoid structure and such that Mˣ is torsion-free, then M is torsion-free.

Note. You need to import this file to get that the monoid of ideals of a Dedekind domain is torsion-free.

theorem HasUniqueRoots.mk' {M : Type u_1} [CommMonoidWithZero M] [IsReduced M] (ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y) : HasUniqueRoots M

@[deprecated HasUniqueRoots.mk' (since := "2026-08-07")]

theorem IsMulTorsionFree.mk' {M : Type u_1} [CommMonoidWithZero M] [IsReduced M] (ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y) : HasUniqueRoots M

Alias of HasUniqueRoots.mk'.

instance UniqueFactorizationMonoid.instHasUniqueRoots {M : Type u_1} [CommMonoidWithZero M] [UniqueFactorizationMonoid M] [NormalizationMonoid M] [IsMulTorsionFree Mˣ] : HasUniqueRoots M