# Commit 2022-11-19 14:36 bc5c9b40

View on Github →feat(ring_theory/ideal): define absolute ideal norm (#17203)
This PR defines the absolute ideal norm `ideal.abs_norm`

on a number ring (specifically, a Dedekind domain that is a finite, free extension of ℤ) as the finite cardinality of the quotient ideal (and zero if the cardinality is infinite).