Commit 2023-02-03 19:48 85e3c05a
View on Github →feat(ring_theory/ideal/norm): relative ideal norm (#18303)
This PR contains the definition of ideal.rel_norm, the relative ideal norm as a bundled monoid-with-zero homomorphism sending I : ideal S to the ideal in R spanned by the norms of the elements in I; here R and S are Dedekind domains and S is an extension of R which is finite free as an R-module.
Co-Authored-By: Alex J. Best alex.j.best@gmail.com