Commit 2025-05-16 09:35 c6c9ebee

feat(RingTheory/Ideal): An ideal of ℤ is generated by its norm (#24933) We also prove that

• x and |x| are associated
• x and |x| span the same ideal Note however that the proof of the second result does not use the first result since that would require commutativity but the result is also true in the noncommutative case.