mathlib3

93def16e - feat(analysis/normed/ring/seminorm): Multiplicative ring norms (#16766)

feat(analysis/normed/ring/seminorm): Multiplicative ring norms (#16766) Define `mul_ring_seminorm`/`mul_ring_norm`, the type of multiplicative `ring_seminorm`/`ring_norm`.