feat(DedekindDomain): Monoid of ideals is torsion-free (#28169)

We prove that an unique factorization monoid `M` that can be equipped with a
`NormalizationMonoid` structure and such that `Mˣ` is torsion-free, is torsion-free.

As consequence, we get the instance
```
import Mathlib.Algebra.GroupWithZero.Torsion
import Mathlib.RingTheory.DedekindDomain.Ideal.Basic

variable {R : Type*} [CommRing R] [IsDedekindDomain R]

instance : IsMulTorsionFree (Ideal R) := inferInstance
```

Note: the lemma `Associated.pow_iff` comes with a previous version of the proof and is not used in the current proof but was left since it may be useful anyway

Co-authored-by: Kenny Lau  <kc_kennylau@yahoo.com.hk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>

Author: xroblot

Mathlib.lean

@@ -497,6 +497,7 @@ import Mathlib.Algebra.GroupWithZero.Shrink
 import Mathlib.Algebra.GroupWithZero.Subgroup
 import Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
 import Mathlib.Algebra.GroupWithZero.Submonoid.Primal
+import Mathlib.Algebra.GroupWithZero.Torsion
 import Mathlib.Algebra.GroupWithZero.TransferInstance
 import Mathlib.Algebra.GroupWithZero.ULift
 import Mathlib.Algebra.GroupWithZero.Units.Basic

Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

@@ -227,4 +227,8 @@ theorem sum_map_tsub [AddCommMonoid M] [PartialOrder M] [ExistsAddOfLE M]
 
 end OrderedSub
 
+instance {M : Type*} : IsAddTorsionFree (Multiset M) :=
+  ⟨fun n hn x y h ↦ open Classical in Multiset.ext' fun _ ↦
+    (Nat.mul_right_inj hn).mp <| by simp only [← Multiset.count_nsmul, h]⟩
+
 end Multiset

Mathlib/Algebra/Group/Torsion.lean

@@ -35,6 +35,10 @@ lemma pow_left_injective (hn : n ≠ 0) : Injective fun a : M ↦ a ^ n :=
 @[to_additive nsmul_right_inj]
 lemma pow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (pow_left_injective hn).eq_iff
 
+@[to_additive]
+lemma IsMulTorsionFree.pow_eq_one_iff (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 :=
+  ⟨fun h ↦ by rwa [← pow_left_inj hn, one_pow], fun h ↦ by rw [h, one_pow]⟩
+
 end Monoid
 
 section Group

Mathlib/Algebra/GroupWithZero/Associated.lean

@@ -72,6 +72,9 @@ end Associated
 
 attribute [local instance] Associated.setoid
 
+theorem Associated.of_eq [Monoid M] {a b : M} (h : a = b) : a ~ᵤ b :=
+  ⟨1, by rwa [Units.val_one, mul_one]⟩
+
 theorem unit_associated_one [Monoid M] {u : Mˣ} : (u : M) ~ᵤ 1 :=
   ⟨u⁻¹, Units.mul_inv u⟩
 

Mathlib/Algebra/GroupWithZero/Torsion.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Xavier Roblot
+-/
+import Mathlib.Algebra.Regular.Basic
+import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
+
+/-!
+# 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.
+-/
+
+variable {M : Type*} [CancelCommMonoidWithZero M]
+
+theorem IsMulTorsionFree.mk' (ih : ∀ x ≠ 0, ∀ y ≠ 0, ∀ n ≠ 0, (x ^ n : M) = y ^ n → x = y) :
+    IsMulTorsionFree M := by
+  refine ⟨fun n hn x y hxy ↦ ?_⟩
+  by_cases h : x ≠ 0 ∧ y ≠ 0
+  · exact ih x h.1 y h.2 n hn hxy
+  grind [pow_eq_zero, zero_pow]
+
+variable [UniqueFactorizationMonoid M] [NormalizationMonoid M] [IsMulTorsionFree Mˣ]
+
+namespace UniqueFactorizationMonoid
+
+instance : IsMulTorsionFree M := by
+  refine .mk' fun x hx y hy n hn hxy ↦ ?_
+  obtain ⟨u, hu⟩ : Associated x y := by
+    have := (Associated.of_eq hxy).normalizedFactors_eq
+    rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
+      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
+  replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n
+  rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
+    Units.val_eq_one, IsMulTorsionFree.pow_eq_one_iff hn] at hxy
+  rwa [hxy, Units.val_one, mul_one] at hu
+
+end UniqueFactorizationMonoid

Mathlib/Algebra/Regular/Basic.lean

@@ -209,4 +209,12 @@ lemma IsRightRegular.pow_iff (n0 : 0 < n) : IsRightRegular (a ^ n) ↔ IsRightRe
   mp h := ⟨(IsLeftRegular.pow_iff n0).mp h.left, (IsRightRegular.pow_iff n0).mp h.right⟩
   mpr h := ⟨.pow n h.left, .pow n h.right⟩
 
+@[to_additive (attr := simp)] lemma IsLeftRegular.mul_left_eq_self_iff (ha : IsLeftRegular a) :
+    a * b = a ↔ b = 1 :=
+  ⟨fun h ↦ by rwa [← ha.eq_iff, mul_one], fun h ↦ by rw [h, mul_one]⟩
+
+@[to_additive (attr := simp)] lemma IsRightRegular.mul_right_eq_self_iff (ha : IsRightRegular a) :
+    b * a = a ↔ b = 1 :=
+  ⟨fun h ↦ by rwa [← ha.eq_iff, one_mul], fun h ↦ by rw [h, one_mul]⟩
+
 end Monoid

Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

@@ -258,6 +258,12 @@ theorem pow_dvd_pow_iff [IsDomain R] [IsIntegrallyClosed R]
   refine ⟨k, IsFractionRing.injective R K ?_⟩
   rw [map_mul, hk, mul_div_cancel₀ _ ha]
 
+@[simp]
+theorem _root_.Associated.pow_iff [IsDomain R] [IsIntegrallyClosed R] {n : ℕ} (hn : n ≠ 0)
+    {a b : R} :
+    Associated (a ^ n) (b ^ n) ↔ Associated a b := by
+  simp_rw [← dvd_dvd_iff_associated, pow_dvd_pow_iff hn]
+
 variable (R)
 
 /-- This is almost a duplicate of `IsIntegrallyClosedIn.integralClosure_eq_bot`,