Commit 2026-10-23 11:31 25707135

chore(RingTheory/Ideal/Norm): restate the Ideal.absNorm API for rings with finite quotients (#42790) Most results about absNorm that assumed [Module.Finite ℤ S] are restated for a ring with finite quotients under a primed name, the original version is kept and proved using the new one. The plan is to eventually keep only the primed versions, under their unprimed names. This is not done here because Ring.HasFiniteQuotients S does not follow by instance search from [Module.Finite ℤ S], so it seems better to do that separately. A few results no longer need the ring to be infinite either, now that the norm has the junk value 0 at the zero ideal. The body of the file is reorganized accordingly, in four blocks: the results needing no finiteness assumption, those over an infinite ring, those over a ring with finite quotients, and those over a ring finite over ℤ. Prepared with Claude Code 🤖