Commit 2023-01-31 16:05 8233a1cb

View on Github →

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.

Estimated changes

Modified src/ring_theory/ideal/norm.lean

added theorem ideal.map_span_norm

added theorem ideal.norm_mem_span_norm

added def ideal.span_norm

added theorem ideal.span_norm_bot

added theorem ideal.span_norm_localization

added theorem ideal.span_norm_mono

added theorem ideal.span_norm_singleton

added theorem ideal.span_norm_top