…d_submonoid.closure` (#18854)

Per [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Star.20ordered.20ring), this refactors `star_ordered_ring` so that the condition `star_ordered_ring.nonneg_iff` is changed from `∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s` to something morally equivalent to `∀ x : R, 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range (λ s : R, star s * s))`.

In fact, we actually change the structure field `nonneg_iff` to `le_iff`, which characterizes `· ≤ ·` instead of just `0 ≤ ·`. When `R` is a `non_unital_ring`, there is effectively no change (see how we recover `star_ordered_ring.nonneg_iff` and also `star_ordered_ring.of_nonneg_iff`), but it gives a more useful and sensible condition when `R` is only a `non_unital_semiring`. For instance, now `conjugate_le_conjugate` holds for `non_unital_semiring`. 

There are essentially two reasons for this change.
1. It would be nice if things like `ℚ` could be `star_ordered_ring`s. This is a minor reason, but it should be a nice convenience. This instance is added in this PR in a new file.
2. Much more importantly, we want to declare the positive elements in a `star_ordered_ring` as an `add_submonoid`, but to accomplish this with the previous definition requires much more stringent type class assumptions (e.g., C⋆-algebras) and sophisticated machinery (the continuous functional calculus) in order to show that the sum of positive elements is positive. This change essentially allows us to defer that proof obligation to the settings where it will matter that a positive element really does have the form `star s * s`.

We remark that even for C⋆-algebras, the fact that the sum of positive elements (i.e., those of the form `star s * s`) is positive is a deep result which was first shown in 1952 by [Fukamiya](http://www.sci.kumamoto-u.ac.jp/~kjm/BKS/kjmpdf/KJSM/v1-4-fukamiya.pdf), and then again in 1953 by [Kelley and Vaught](https://www.ams.org/journals/tran/1953-074-01/S0002-9947-1953-0054175-2/S0002-9947-1953-0054175-2.pdf). These proofs are in essence very similar, but the latter is more aesthetically pleasing, and it is this proof that appears in all the textbooks. I went looking and did not see another proof anywhere in the literature.

We provide a few convenience constructors for `star_ordered_ring` in the form of reducible definitions which can apply when `R` is either a `non_unital_ring` (so we only need to characterize nonnegativity), and / or when positive elements have exactly the form `star s * s`. In this way, we can effectively maintain the status quo (see the instances for `real` and `complex`).

This forward-ports all the files from leanprover-community/mathlib3#18854 which have already been ported, and it also ports the new file `algebra.star.order`, which is a split from `algebra.star.basic` and was necessary to do at the same time.



Co-authored-by: Chris Hughes <chrishughes24@gmail.com>