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).

Estimated changes