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 IsMulTorsionFree.mk' {M : Type u_1} [CommMonoidWithZero M] [NoZeroDivisors M] (ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y) : IsMulTorsionFree M

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