mathlib3

97befb83 - feat(analysis/normed/ring/seminorm): add ring_seminorm, ring_norm (#14115)

feat(analysis/normed/ring/seminorm): add ring_seminorm, ring_norm (#14115) We define structures `ring_seminorm` and `ring_norm`. These definitions are useful when one needs to consider multiple (semi)norms on a given ring. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>