Commit 2026-08-15 05:01 971f540b

chore(RingTheory/Ideal/Norm): move the cardQuot finiteness API into AbsNorm (#42784) Several results in Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients/Norm.lean only involve Submodule.cardQuot and the class Ring.HasFiniteQuotients, not Ideal.absNorm. They lived there only because AbsNorm.lean could not import the class; since #42081 it can, so they are moved next to cardQuot. The file HasFiniteQuotients/Norm.lean keeps the two Northcott instances. The absNorm finiteness results are golfed into corollaries of finite_cardQuot_le, which also lets us drop their [CharZero S] hypothesis. This move is also what makes the next step possible: once Ideal.absNorm is weakened to [Ring.HasFiniteQuotients S], some proofs in AbsNorm.lean have to call one of these results, but those lemmas cannot be reached from AbsNorm.lean as long as they live in a file importing it. This is the second part of a sequence of PRs generalizing Ideal.absNorm away from Module.Free ℤ, after #42081. Prepared with Claude Code 🤖