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).
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
