mathlib3

8233a1cb - feat(ring_theory): definition and properties of relative ideal norm (#18299)

feat(ring_theory): definition and properties of relative ideal norm (#18299) This PR provides a definition of the relative ideal norm `ideal.span_norm R I` as the ideal spanned by the norms of elements in `I`. We also give some basic results on this definition. A follow-up PR will bundle this into a homomorphism `ideal.rel_norm`.