feat(algebra/star): star_ordered_ring (#4685)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: kim-em

src/algebra/ordered_ring.lean

@@ -828,6 +828,10 @@ instance linear_ordered_comm_ring.to_integral_domain [s : linear_ordered_comm_ri
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_comm_ring.to_linear_ordered_semiring [d : linear_ordered_comm_ring α] :
    linear_ordered_semiring α :=
+-- One might hope that `{ ..linear_ordered_ring.to_linear_ordered_semiring, ..d }`
+-- achieved the same result here.
+-- Unfortunately with that definition we see mismatched `preorder ℝ` instances in
+-- `topology.metric_space.basic`.
 let s : linear_ordered_semiring α := @linear_ordered_ring.to_linear_ordered_semiring α _ in
 { zero_mul                   := @linear_ordered_semiring.zero_mul α s,
   mul_zero                   := @linear_ordered_semiring.mul_zero α s,

src/algebra/star/basic.lean

@@ -150,3 +150,17 @@ local attribute [instance] star_ring_of_comm
 @[simp] lemma star_id_of_comm {R : Type*} [comm_semiring R] {x : R} : star x = x := rfl
 
 end
+
+/--
+An ordered *-ring is a ring which is both an ordered ring and a *-ring,
+and `0 ≤ star r * r` for every `r`.
+
+(In a Banach algebra, the natural ordering is given by the positive cone
+which is the closure of the sums of elements `star r * r`.
+This ordering makes the Banach algebra an ordered *-ring.)
+-/
+class star_ordered_ring (R : Type u) [ordered_semiring R] extends star_ring R :=
+(star_mul_self_nonneg : ∀ r : R, 0 ≤ star r * r)
+
+lemma star_mul_self_nonneg [ordered_semiring R] [star_ordered_ring R] {r : R} : 0 ≤ star r * r :=
+star_ordered_ring.star_mul_self_nonneg r