Commit 2021-03-31 09:30 1fdce2f8
View on Github →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
.