Commit 2026-10-23 16:22 5e9fd0e0

chore(RingTheory/Ideal): drop the infiniteness assumption from the results using Ideal.absNorm (#44646) Now that the absolute norm of an ideal has the junk value 0 at the zero ideal, the results using it no longer need the ring to be infinite. This assumption is dropped from Ideal.absNorm_under_dvd_absNorm and from the results on finite places and adeles of a Dedekind domain with finite quotients. Prepared with Claude Code 🤖