basic): Non-linear normed ordered groups (#17238)

Commit

3 years ago

feat(analysis/normed/order/basic): Non-linear normed ordered groups (#17238) Define `normed_ordered_add_group`. Also multiplicativise everything.

Author

YaelDillies

Parents