Commit 2026-08-31 14:42 52d7ff78

chore(RingTheory/Ideal/Norm): weaken Ideal.absNorm to infinite Dedekind domains (#42787) Ideal.absNorm and Submodule.cardQuot_mul assumed Module.Free ℤ S, where all that is really needed is Infinite S. They now assume the latter, which brings in rings that are not finite over ℤ. The results genuinely using a ℤ-basis are collected in a section Free. Downstream, several lemmas therefore assume Infinite where they assumed Module.Free ℤ. This is not a real restriction: the instance should hold for every ring these results are applied to, and should simply be added when missing, independently of this PR. This is the third part of a sequence of PRs generalizing Ideal.absNorm away from Module.Free ℤ, after #42081 and #42784. Prepared with Claude Code 🤖