Commit 2025-09-01 13:46 30a7c422

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