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