mathlib

7ea60478 - feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms (#16919)

feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms (#16919) Generalise `..._seminorm_class` to arbitrary codomains (rather than just `ℝ`). Instantiate `mul_ring_norm_class` for absolute values.