Commit 2026-10-17 09:16 99d54ff7

refactor(RingTheory/Ideal/Norm): give Ideal.absNorm the junk value 0 at ⊥ (#44698) The absolute norm of an ideal is now given the junk value 0 at the zero ideal. It is therefore no longer assumed that the ring is infinite, an assumption that was there to get absNorm ⊥ = 0. Three lemmas unfold the norm: Ideal.absNorm_of_ne_bot for a nonzero ideal, with no further assumption, Ideal.absNorm_apply for every ideal of an infinite ring, both stated using Submodule.cardQuot, and Ideal.absNorm_eq_natCard, which is new, giving the same equality in the form absNorm I = Nat.card (S ⧸ I). The results of the file are restated for a ring with finite quotients in #42790, and the results downstream lose their infiniteness assumption in #44646. Prepared with Claude Code 🤖