mathlib3

feat(analysis/normed/ring/seminorm): add `equiv` and nonarchimedean property

#17817

Open