Commit 2022-08-29 08:18 24a233d4

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.