feat(algebra/order/positive): new file (#14833)
Define various algebraic structures on the set of positive numbers.
I have two reasons to introduce these classes:
- we can use `{x : ℝ // 0 < x}` in various filter bases; this may save us from explicit usage of `half_pos` or `div_pos` here or there;
- I want to introduce a multiplicative action of `{x : ℝ // 0 < x}` on the upper half plane.
