Commit 2026-10-27 14:08 8951f3e8

refactor(RingTheory/Ideal/Norm/AbsNorm): state the absNorm finiteness lemmas for rings with finite quotients (#45255) Several lemmas about the absolute norm of an ideal exists in two copies: one for a finite ℤ-module, and a primed version for a ring with finite quotients, the first one being a restatement of the second. In this PR, the primed versions are kept, under the unprimed names, and the duplicates are deprecated. Three finiteness results that had no primed version but were restatements of lemmas in the Ring.HasFiniteQuotients namespace are deprecated in favor of those lemmas, and their uses updated. Note that the lemmas now require Ring.HasFiniteQuotients R rather than Module.Finite ℤ R. Where only the latter is available, the missing instance can be supplied by Ring.HasFiniteQuotients.of_module_finite. The module docstring now advertises Ring.HasFiniteQuotients.finite_cardQuot_le, which is the result the finiteness statements rest on, rather than finite_absNorm_le, as suggested in #42790. Prepared with Claude Code 🤖