Theorems · Inductive type · functional analysis

StarOrderedRing

(R : Type u_3) → [inst : NonUnitalSemiring R] → [PartialOrder R] → [StarRing R] → Prop

An ordered \-ring is a \-ring with a partial order such that the nonnegative elements constitute precisely the AddSubmonoid generated by elements of the form star s * s. If you are working with a NonUnitalRing and not a NonUnitalSemiring, it may be more convenient to declare instances using StarOrderedRing.of_nonneg_iff.

Defined in

Mathlib.Algebra.Order.Star.Basic

Cited by

587 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 6 definitions · uses no axioms

Assumes

NonUnitalSemiringPartialOrderStarRing