mathlib

1fdce2f8 - refactor(analysis/normed_space/basic): add semi_normed_ring (#6889)

refactor(analysis/normed_space/basic): add semi_normed_ring (#6889) This is the natural continuation of #6888 . We add here semi_normed_ring, semi_normed_comm_ring, semi_normed_space and semi_normed_algebra. I didn't add `semi_normed_field`: the most important result for normed_field is `∥1∥ = 1`, that is false for `semi_normed_field`, making it a more or less useless notion. In particular a `semi_normed_space` is by definition a vector space over a `normed_field`.